PolyCore is an Associate Team with INRIA project-team Espresso and the Fermat Laboratory at Virginia Tech, created in 2011.
Anyone experienced with multi-threaded programming would recognize the difficulty of designing and implementing such software. Resolving concurrency, synchronization, and coordination issues, and tackling the non-determinism germane in multi-threaded software is extremely difficult. Ensuring correctness with respect to the specification and deterministic behavior is necessary for safe execution of such code. It is therefore desirable to synthesize multi-threaded code from formal specifications using a provably `correct-by-construction' approach. In Europe, it has been widely claimed that the embedded software for 'fly-by-wire' was mostly automatically generated using tools based on the synchronous programming models. Unfortunately, software generated in those contexts usually operate in a time-triggered execution model. Such models are simpler but less efficient than multi-threaded software on multi-core processors. Normally they run on multiple processors communicating over a time-triggered bus. Hence the execution is less efficient than it could be. While time-triggered programming model simplifies code generation, we feel that multi-rate event driven execution model is much more efficient. Code synthesis for such execution model must be thoroughly investigated. The multi-threaded software generation is inspired by a recent shift in the hardware design paradigms from single-core to multi-core processors. This shift has brought parallel and concurrent programming to the desktop and embedded arena. In the desktop market, most processors now being sold are multi-core, and very soon this trend might conquer the embedded world as well. We plan to develop formal models, methods, algorithms and techniques for generating provably correct multi-threaded reactive real-time embedded software for mission-critical applications. For scalable modeling of larger embedded software systems, the specification formalism has to be compositional and hierarchical. Our proposed formalism entails a model of computation (MoC) based on a multi-rate synchronous data-flow paradigm: Polychrony.
The three most important requirements for the mission-critical embedded systems are: correctness, timeliness and resilience to faults. An alternative approach to correctness is post-programming formal verification but today's formal verification tools are severely capacity limited and techniques for compositional, assume/guarantee reasoning for verification are not fully developed yet. Even after much sophisticated programming and testing, we have many examples such as the priority inversion in the Mars Rover software or Toyota, where subtle bugs escape even the best programmers and testers. Currently, common practice in the industry is to use tools such as MATLAB/Simulink to create simulation models, and then either manually translate or automatically generate code. However, this or other similar academic systems are not endowed with proper formal semantics, and hence the generated code needs thorough verification before release for production usage. In fact, most of these cannot even generate multi-threaded code, or are at their infancy in doing so. However, recent efforts have been made in providing formal semantics to Simulink block diagram languages (e.g. in the GeneAuto project) and some similar efforts in verification have also been undertaken in the recent years. We propose to develop a formal framework or modeling formalism for capturing specifications for multi-rate reactive concurrent embedded systems. Our early formal analytical results show that our formalism is effective for provably correct mission-critical deterministic multi-threaded code synthesis. The project will study
Therefore, in this project we target multi-core platforms and the code generation challenges for multi-threaded embedded software. The requirements are that the generated code must be deterministic and predictable despite the multi-threading, must provide timing guarantees when required, and must be resilient or dependable in the face of various types of common fault types. In this project, we believe we have theopportunity to make a wide impact in the industry and academia alike.
Jean-Pierre Talpin (INRIA, DR) Loïc Besnard (CNRS, IR) Paul Le Guernic (INRIA, DR) Thierry Gautier (INRIA, CR) Huafeng Yu (INRIA, Post-doctorate) Sun Ke (INRIA, PhD. Student)
Sandeep Shukla (Professor) Julien Ouy (Post-doctorate) Jing Huang (Post-doctorate) Yi Deng (Post-doctorate) Matthew Anderson (PhD. Student) Mahesh Nanjundappa (PhD. Student)
Klaus Schneider (Professor) Jens Brandt (Assistant Professor) Mike Gemunde (Post-doctorate)
Sandeep Shukla and Jean-Pierre Talpin co-edited a special section of the IEEE Transactions on Computers entitled "Science of design for safety critical systems".
R. K. Shiamasundar (TIFR) invited Sandeep Shukla, Klaus Schneider and Jean-Pierre Talpin as co-editors on a special issue of the CSI Journal on Computing on synchronous programming.
Together with the official release of the Polychrony toolbox in open-source by INRIA in July 2011, through this year's visits and the subsequent joint research which followed, we have established a strong community among our research teams to co-develop new tools and programming languages, based on the MRCIDF framework by Virginia Tech and on the Quartz programming environment of the ESG. Some first publications outline the longer path before us in this direction.
Our main achievement this year was a joint decision to merge these two existing collaborations, between Virginia Tech and the Espresso project-team, and between Virginia Tech and the ESG, in order to best meet the challenges of the Polycore project with the program detailed in the next section. We would like the visiting program of Polycore to extend to members of the ESG. In addition, we are presently submitting a joint research proposal, entitled "Component-based synthesis of deterministic multi-threaded programs on multi-core embedded architectures", for funding by the US Air Force Laboratories, to provide additional funding for visits and, possibly, a joint post-doctorate researcher position.
This year, we did further the theoretical background and scale the implementation and experiments of the Polycore framework by starting the development of a domain-specific language, called Onyx, build from synchronous modules designed with Quartz, an imperative synchronous programming language, and connected by data-flow networks described in Signal, the polychronous data-flow language at the core of Polychrony. We believe that the combination of viewpoints and paradigms offered by these two design environments provides powerful abstractions and easy to use concepts in order to address two design challenges :
1/ to provide a natural and dependable specification of elementary synchronous functionalities, most of them algorithmic and control-intensive, in the imperative framework offered by Quartz.
2/ to automatically synthesize the scheduling of computations and communications among these functionalities starting from the multi-clocked synchronous abstractions offered by the Signal data-flow language.
This year, we have two journal articles accepted for publication in IEEE TSE and Springer DAEM, one conference paper published in FDL and another submitted in FSTTCS.
In June 2012, we jointly organized the 10th. edition of the ACM-IEEE MEMOCODE conference (a conference which we created in the frame of the former BALBOA associate project) at the Virginia Tech conference center in Arlington.
We wish to pursue our main goal of jointly implementing a synchronous/polychronous co-modeling framework in project Polycore. The capability of Polychrony to serve as infrastructure for that purpose was demonstrated at large by a joint case study with IRIT and Airbus (figure, published in ACM SAC'11) in which we considered co-modeling the doors management system of the A350. In this case study, we considered functionalities modeled with synchronous Simulink and a system-level model of the hardware equipment specified in AADL. We beleive that using the Polychrony environment for that purpose offers the right model of computations and communications and the appropriate toolbox to help in the development of our domain-specific language: Onix.
In 2012-2013, we plan to submit a joint project proposal with TU Kaiserslautern, Virginia Tech Arlington and the Naval Research Laboratory on the scientific themes of the Polycore project.
Jean-Pierre Talpin visited Virginia Tech for 10 days in May 2011 to work on extending program analysis in polychrony to SMT-solving capabilities.
Loic Besnard visited Virginia Tech during two weeks in June 2011 to provide extensive support to the FERMAT team with using and developping the now open-source Polychrony environment.
Jens Brandt (Universitaet Kaiserslautern) visited INRIA-Rennes for a week in June 2011 to initiate a joint collaborative project with Virginia Tech on building a common multi-clocked synchronous programming environment based on Polychrony (ESPRESSO team) and Quartz (U. Kaiserslautern)
Jean-Pierre Talpin visited Virginia Tech for two weeks in September 2011 to work on a joint collaboration proposal with Virginia Tech, Universitaet Kaiserslautern funded by the US Air Force Laboratories. He gave an invited talk on Polychrony at the CESCA seminar at Virginia Tech.
Julien Ouy (Virginia Tech) visited INRIA-Rennes for one week in February 2012.
Jens Brandt, Mike Gemuende (TU Kaiserslautern) and Sandeep Shukla (Virginia Tech) visited INRIA-Rennes for one week in May 2012. They are planing a second visit in November, prior to the Synchron 2012 workshop, organized by INRIA-Rennes.
Jean-Pierre Talpin visited TU Kaiserslautern for one day in June 2012 during a Dagstuhl meeting. He plans a second meeting at Virginia Tech in October 2012.
Jens Brandt, Mike Gemuende (TU Kaiserslautern) and Sandeep Shukla (Virginia Tech) and Jean-pierre Talpin meet at Virginia Tech Conference Centre in Arlington, after ACM/IEEE MEMOCODE, in July 2012.
We are planing the following visits for next year
for an estimated funding request of 10000 euros.
"Programming models for multi-core embedded systems" Jose, B., Xue, B., Shukla, S., Talpin, J.-P. Chapter in Multi-core Embedded Systems. Taylor and Francis, 2009.
"Compositional behavioral modeling of embedded systems and conformance checking" Talpin, J.-P, Le Guernic, P., Shukla, S., Gupta, R. In International Journal on Parallel processing, special issue on testing of embedded systems. Springer Verlag, 2005.
"Behavioral type inference for compositional system design" Talpin, J.-P., Berner, D., Shukla, S., Le Guernic, P., Gamatié, A., Gupta, R. Chapter in Formal Methods and Models for System Design. Kluwer Academic Publishers, 2004.
"Capturing formal specifications into abstract models" Berner, D., Suhaib, S., Shukla, S., Talpin, J.-P. Chapter in Formal Methods and Models for System Design. Kluwer Academic Publishers, 2004.
"Formal refinement checking in a system-level design methodology" Talpin, J.-P., Le Guernic, P., Shukla, S. K., Gupta, R., Doucet, F. Special Issue of Fundamenta Informaticae on Applications of Concurrency to System Design. IOS Press, 2004.
"Distributed simulation of AADL specifications in a polychronous model of computation" Ma, Y., Talpin, J.-P.,Shukla, S., Gautier, T. International Conference on Embedded Software and Systems (ICESS'09). IEEE Press, 2009.
"On the automatic inference of synchronization logic for multi-threaded software synthesis from polychronous specifications" Jose, B., Shukla, S., Patel, H., Talpin, J.-P. ACM-IEEE Conference on Methods and Models for Codesign (MEMOCODE'08). IEEE, June 2008.
"Generating multi-threaded code from polychronous specifications" Jose, B., Patel, H., Shukla, S., Talpin, J.-P. Synchronous Languages, Applications, and Programming (SLAP'08). Elsevier, March 2008.
"On the polychronous approach to embedded software design" Shukla, S. K., Suhaib, S. M., Mathaikutty, D. A., Talpin, J.-P. Next generation design and verification methodologies for distributed embedded systems (GM R&D WORKSHOP'07). Springer Verlag, 2007.
"Polychronous methodology for system design, a true concurrency approach" S. Suhaib, D. Mathaikutty, S. Shukla, J.-P. Talpin. High-level design, validation and test workshop (HLDVT'06). IEEE Press, November 2006.
"Automated clock inference for stream function-based system level specifications" Talpin, J.-P., Shukla, S. High-level design, validation and test workshop (HLDVT'05). IEEE Press, November 2005.
"SystemCXML: an open-source extensible SystemC front-end using XML" Berner, D., Patel, H., Mathaikutty, D., Shukla, S., Talpin, J.-P. Forum on Specification and Design Languages (FDL'05). ECSI, September 2005.
"A verification approach for GALS integration of synchronous components" Doucet, F., Menarini, M., Krueger, I., Talpin, J.-P., Gupta, R. International Workshop on Formal Methods for Globally Asynchronous locally Synchronous Design (FMGALS'05). Electronic Notes in Computer Science. Elsevier, June 2005.
"A functional programming framework for latency insensitive protocol validation" Suhaib, S., Mathaikutty, D., Shukla, S., Berner, D., Talpin, J.-P. International Workshop on Formal Methods for Globally Asynchronous locally Synchronous Design (FMGALS'05). Electronic Notes in Computer Science. Elsevier, June 2005.
"Modular design through component abstraction" Berner, D., Talpin, J.-P., Le Guernic, P., Shukla, S. K. International conference on compilers, architectures and synthesis for embedded systems (CASES'04). ACM Press, September 2004.
"A behavioral type inference system for compositional system-on-chip design" Talpin, J.-P., Berner, D., Shukla, S. K., Gamatié, A., Le Guernic, P., Gupta, R. Application of Concurrency to System Design (ACSD'04). IEEE Press, June 2004.
"Formal methods and models for system design: a system-level perspective". Gupta, R., Le Guernic, P., Shukla, S., Talpin, J.-P., Editors. ISBN 1-4020-8051-4 Springer Verlag, 2004
For more information The Espresso project team at INRIA Rennes
The Fermat laboratory at Virginia Tech
The Embedded Systems Group at Universitaet Kaiserslautern
ContactsJean-Pierre.Talpin at inria.fr
Sandeep.Shhukla at vt.edu
Klaus.Schneider at uni-kl.de
