A New Multi-threaded Code Synthesis Methodology and Tool for Correct-by-Construction Synthesis from Polychronous Specifications

Embedded software systems respond to multiple events coming from various sources - some temporally regular (ex: periodic sampling of continuous time signals) and some intermittent (ex: interrupts, exception events etc.). Timely response to such events while executing complex computation, might require multi-threaded implementation. For example, overlapping I/O of various types of events, and computation on such events may be delegated to different threads. However, manual programming of multi-threaded programs is error-prone, and proving correctness is computationally expensive. In order to guarantee safety of such implementations, we believe that a correct-by-construction synthesis of multi-threaded software from formal specification is required. It is also imperative that the multiple threads are capable of making progress asynchronous to each other, only synchronizing when shared data is involved or information requires to be passed from one thread to other. Especially on a multi-core platform, lesser the synchronization between threads, better will be the performance. Also, the ability of the threads to make asynchronous progress, rather than barrier synchronize too often, would allow better real-time schedulability. In this work, we describe our technique for multi-threaded code synthesis from a variant of the polychronous programming language SIGNAL, namely MRICDF. Through a series of experimental benchmarks we show the efficacy of our synthesis technique. Our tool EmCodeSyn which was built originally for sequential code synthesis from MRICDF models has been now extended with multi-threaded code synthesis capability. Our technique first checks the concurrent implementability of the given MRICDF model. For implementable models, we further compute the execution schedule and generate multi-threaded code with appropriate synchronization constructs so that the behavior of the implementation is latency equivalent to that of the original MRICDF model.