SMT based false causal loop detection during code synthesis from Polychronous specifications

Bijoy Anthony Jose 1 Abdoulaye Gamatié 2 Julien Ouy 1 Sandeep Kumar Shukla 1
2 DART - Contributions of the Data parallelism to real time
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
Abstract : Polychronous specifications express concurrent, multi-clocked models which capture multiple threads of computation operating relatively asynchronous to each other. A clock of a variable in this context, is the totally ordered set of instants at which events occur on that variables. However, the notion of instant here is logical as opposed to real-time instants. The instants of different clocks may be partially ordered. The executable code synthesis from Polychronous specifications relies on computation of schedules through clock calculus. Unfortunately, it is often hard to distinguish from true causal loops which cause deadlocks from apparent causal loops which do not. The SIGNAL compiler in the Polychrony tool-set currently rejects all programs with apparent causal loops, thus rejecting a large set of valid specifications. A recently developed polychronous formalism MRICDF and its tool-set EmCodeSyn do the same. Even in the Polychrony literature, the deadlock causing loop detection based on Boolean satisfiability is not enough to discern all possible false loops, thereby still rejecting a lot of valid specifications. In order to not reject programs whose apparent loops are never realizable, a theory of reals or integers or other data types are required. In this paper, we formulate the detection of false loops in MRICDF as a decision problem in Satisfiability Modulo Theory (SMT). Due to recent interests in SMT solvers, a number of efficient solvers are available which offer a greater expressiveness in dealing with non Boolean constraints and allow us to discern false loops from realizable causalities in reasonable computation time. This paper proposes an SMT based synthesis technique which demonstrates that several polychronous specifications rejected by the Polychrony/EmCodeSyn synthesis tools due to their inability to identify only true causal loops, can be synthesized as correct sequential embedded software.
Type de document :
Communication dans un congrès
9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), Jul 2011, Cambridge, United Kingdom. 2011, 〈10.1109/MEMCOD.2011.5970517〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00637574
Contributeur : Mister Dart <>
Soumis le : mercredi 2 novembre 2011 - 13:53:44
Dernière modification le : jeudi 11 janvier 2018 - 06:22:13

Identifiants

Collections

Citation

Bijoy Anthony Jose, Abdoulaye Gamatié, Julien Ouy, Sandeep Kumar Shukla. SMT based false causal loop detection during code synthesis from Polychronous specifications. 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), Jul 2011, Cambridge, United Kingdom. 2011, 〈10.1109/MEMCOD.2011.5970517〉. 〈inria-00637574〉

Partager

Métriques

Consultations de la notice

168