Skip to Main content Skip to Navigation
Reports

Liquid Clocks - Refinement Types for Time-Dependent Stream Functions

Abstract : The concept of liquid clocks introduced in this paper is a significant step towards a more precise compile-time framework for the analysis of synchronous and polychromous languages. Compiling languages such as Lustre or SIGNAL indeed involves a number of static analyses of programs before they can be synthesized into executable code, e.g., synchronicity class characterization, clock assignment, static scheduling or causality analysis. These analyses are often equivalent to undecidable problems, necessitating abstracting such programs to provide sound yet incomplete analyses. Such abstractions unfortunately often lead to the rejection of programs that could very well be synthesized into deterministic code, provided abstraction refinement steps could be applied for more accurate analysis. To reduce the false negatives occurring during the compilation process, we leverage recent advances in type theory -- with the definition of decidable classes of value-dependent type systems -- and formal verification, linked to the development of efficient SAT/SMT solvers, to provide a type-theoretic approach that considers all the above analyses as type inference problems. In order to simplify the exposition of our new approach in this paper, we define a refinement type system for a minimalistic, synchronous, stream-processing language to concisely represent, analyse, and verify logical and quantitative properties of programs expressed as stream-processing data-flow networks. Our type system provides a new framework to represent logical time (clocks) and scheduling properties, and to describe their relations with stream values and, possibly, other quantas. We show how to analyze synchronous stream processing programs (à la Lustre, Signal) to enable previously described analyzes involved in compiling such programs. We also prove the soundness of our type system and elaborate on the adaptability of this core framework by outlining its extensibility to specific models of computations and other quantas.
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download

https://hal.inria.fr/hal-01166350
Contributor : Jean-Pierre Talpin <>
Submitted on : Thursday, August 13, 2015 - 2:46:02 PM
Last modification on : Monday, May 3, 2021 - 8:44:04 AM
Long-term archiving on: : Wednesday, April 26, 2017 - 9:56:46 AM

File

report.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

  • HAL Id : hal-01166350, version 3

Citation

Jean-Pierre Talpin, Pierre Jouvelot, Sandeep Kumar Shukla. Liquid Clocks - Refinement Types for Time-Dependent Stream Functions. [Research Report] RR-8747, INRIA Rennes - Bretagne Atlantique; INRIA. 2015. ⟨hal-01166350v3⟩

Share

Metrics

Record views

1235

Files downloads

557