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)

1 FERMAT Lab
2 DART - Contributions of the Data parallelism to real time

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.

Mots clés: Boolean constraint; Boolean satisfiability modulo theory; SMT based false causal loop detection; SMT based synthesis technique; SMT solver; clock calculus; discern false loop detection; executable code synthesis; multiclocked model; ordered set; polychronous formalism MRICDF; polychronous specification; polychrony tool set; real-time instants; sequential embedded software; signal compiler; tool set EmCodeSyn; computability; embedded systems; formal specification; program control structures

Domaines: Systèmes embarqués

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. ⟨10.1109/MEMCOD.2011.5970517⟩. ⟨inria-00637574⟩