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.
Type de document :
Rapport
[Research Report] RR-8747, INRIA Rennes - Bretagne Atlantique; INRIA. 2015
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01166350
Contributeur : Jean-Pierre Talpin <>
Soumis le : jeudi 13 août 2015 - 14:46:02
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : mercredi 26 avril 2017 - 09:56:46

Fichier

report.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

742

Téléchargements de fichiers

137