FDL 2018

Forum on specification & Design Languages

@Munich, Germany
September 10-12, 2018

@Munich, Germany


Rainer Domer
University of California, Irvine

1st Keynote: On the Limits of Standard-compliant Parallel Simulation of the IEEE SystemC Language

The IEEE standard 1666 [1] defines SystemC as a C++ class library for system and hardware design. Unfortunately SystemC simulation is based on sequential co-routine semantics, despite the explicit parallelism available in its design models. This imposes strict limits on standard-compliant parallel simulation which obstruct designers’ efforts to increase execution speed by utilizing multi- and many-core host platforms. In this keynote, we discuss seven obstacles [2] identified in the SystemC standard that stand in the way of efficient parallel simulation, including the co-operative multitasking semantics, the weak role of channels, TLM-2.0, and an overall sequential modeling mindset. Thus, truly parallel SystemC appears elusive given the current IEEE standard. Accepting this fact, we can only make the best of it and design parallel SystemC approaches in maximum compliance with the standard.
As an example, we present the Recoding Infrastructure for SystemC (RISC) [3]. RISC is an open source CAD software package that provides a dedicated compiler and simulator for SystemC with out- of-order parallel execution engine, yet maintains the classic transaction level modeling semantics. Experimental results show that RISC can efficiently exploit thread- and data-level parallelism in SystemC models resulting in several hundred times higher simulation speed [4]. We also highlight recent advances in scaling the RISC approach to support large design models with 3rd party library code.

[1] IEEE Computer Society. “IEEE Standard 1666-2011 for Standard SystemC Language Reference Manual”, IEEE, New York, USA, 2011.
[2] R. Dömer: "Seven Obstacles in the Way of Standard-Compliant Parallel SystemC Simulation", IEEE Embedded Systems Letters, vol. 8, no. 4, pp. 81-84, December 2016.
[3] RISC project web site: http://www.cecs.uci.edu/~doemer/risc.html
[4] T. Schmidt, G. Liu, R. Dömer: "Exploiting Thread and Data Level Parallelism for Ultimate Parallel SystemC Simulation", Proceedings of the Design Automation Conference (DAC) 2017, Austin, TX, June 2017.
[5] T. Schmidt, Z. Cheng, R. Dömer: "Port Call Path Sensitive Conflict Analysis for Instance-Aware Parallel SystemC Simulation", Proceedings of the Design, Automation and Test in Europe (DATE) Conference 2018, Dresden, Germany, March 2018.

Rainer Dömer received his Ph.D. degree in Information and Computer Science from the University of Dortmund, Germany, in 2000. He is currently a full Professor in Electrical Engineering and Computer Science at the University of California, Irvine (UCI). He is also a member of the Center for Embedded and Cyber-physical Systems (CECS) at UCI. His research interests include system-level design and methodologies, embedded computer systems, specification and modeling languages, advanced parallel simulation, and the integration of hard- and software systems. Rainer Dömer received the prestigious NSF CAREER Award for his research on efficient modeling of embedded computer systems in 2008, the EECS Faculty of the Year award in 2013, the Best Paper award at the Design, Automation and Test in Europe (DATE) conference in 2014, and the Faculty Innovation in Teaching Mid-Career Award in 2016.

- Web page: http://www.cecs.uci.edu/~doemer/

Jean-Pierre Talpin
INRIA, France

2st Keynote: Refinement types for system design

"Clean-slate" programming environments are now invading territories of general-purpose software development: F*, Liquid Haskell, TypeScript, and to different extends CompCert, Cogent, or even Frama-C, are open-source projects offering one to combine the programming or specification of an application with the proof of its correctness, up to logical requirements specified as dependent types or assertions.
Yet, "shallow" verification with the former languages, as some name it, does not come close to theorem-prover-mechanized certified development with the latter provers, as some advocate. However, the emergence of Cogent (co-generation of program and proof from specification) in SeL4 and, similarly, layered abstractions in CertikOS, manifest the need for modularity and proof abstraction to make verified programming tenable for scalable developments: the SeL4 project revealed the barrier of a quadratic growth of proof obligations w.r.t. the size of code to verify.
And yet, again, modular proof abstraction doesn't seem so different than matured practices of interface-based design, contract-based design, correctness-by-construction, that are most known to the system design community and have been advocated for a decade. Unsurprisingly, this infatuation faced similar quadratic barriers, resulting from the use of automata-based formalisms, and most scaled applications of these methods instead use logical modulo-theory assume-guarantee reasoning.
Clean-state languages are the tools that combine both specification, abstraction and proof capacities by the notion of refinement type {v:Int| v>0} to, e.g., denote the values v of type Int that are strictly positive, and *assume* a function to be called with such numbers and give the opposite *guarantee* on its result: x:{v:Int| v>0} -> {w:Int| w<0}, ergo for arrays, pointers, streams, threads, exceptions, the TLS protocol.
The aim of this keynote is to give the (system) design language community a gentle introduction to the notion of refinement types, at the core of these general-purpose environment, and to demonstrate the potential benefits of such tools in system design by a highlight of orchestrated works in progress in my group: team TEA, and in collaborations with UC San Diego, University of Maryland, IETR, MERCE, the Chinese Academy of Science and Beihang University.

Jean-Pierre Talpin is senior scientist with INRIA and scientific leader of INRIA project TEA. Graduated in Applied Mathematics, he received a Master in Theoretical Computer Science from University Paris VI and did his Ph.D. Thesis at Ecole des Mines de Paris under the supervision of Pierre Jouvelot. He then worked three years as research associate at the European Computer-Industry Research Centre in Munich. He joined INRIA in 1995 and led Inria project ESPRESSO from 2000 to 2012. He is associate editor with the ACM Transaction on Embedded Compter Systems. He edited three books, guest-edited a dozen of scientific journal special issues with ACM and IEEE and authored more than a hundred journal articles, book chapters and conference papers. He received the 2004 ACM Award for the most influential POPL paper, with Mads Tofte, and the 2012 ACM/IEEE LICS Test of Time Award, with Pierre Jouvelot, for his early-carrier work on region inference and region-based memory management. He is the only recipient of both of these awards.

- Web page: http://www.irisa.fr/prive/talpin/

Franz-Josef Grosch
Robert Bosch GmbH

3st Keynote: Blech - a safe synchronous language for embedded real-time programming

Product development at companies such as Bosch requires systems engineering for digital hardware and mechatronic components as well as software engineering for deeply-embedded resource-constrained real-time applications cooperating with distributed cloud applications. While many of the involved engineering disciplines greatly benefit from model-based approaches and from advances in software infrastructures, deeply embedded software is still based on manually written C code, a few components generated from models and glued together with the help of an embedded operating systems like OSEK. Making software safe with the help of tight coding conventions and static analyzers is a time-consuming task. Modern implementation technologies to address software architecture and qualities or to make embedded programming appealing for software professionals are largely missing. We regard synchronous languages to be suitable for solving many of the issues in the integration (causality) and synchronization (clocks) of time-triggered and event-triggered embedded functions that exhibit their behavior over time steps and are coordinated according to their mode-switching in a structured synchronous control flow. Unfortunately, existing synchronous languages do not support modern implementations technologies well such as aggregated data types, object-based programming and separate compilation. Searching for an imperative, strongly-typed, synchronous language (with deterministic concurrent composition, and synchronous control flow), equipped with the aforementioned features for encapsulation and composition (aggregated data types, modules, separate compilation) and supporting programming parallel tasks deployed to separate cores (clock refinement and deterministic inter-task communication), we ended up in designing our own language, suitable for resource-constrained, real-time applications running on multi-core controllers. In this keynote, we will illustrate requirements and features of this language: The realization of synchronous control flow with a focus on separate compilation, a practical way of integrating aggregated data types like arrays, records and references without obstructing causality analysis, and our approach to task-parallel programming. The language design and the compiler implementation is work in progress.

Franz-Josef Grosch is a senior expert at the Bosch Corporate Research campus in Renningen. He studied Computer Science at TU Darmstadt and TU Braunschweig. Franz-Josef worked for several companies as a researcher and software developer. Currently, he works in a department focused on model-based system engineering in the area of software-intensive systems and technologies. The team advances engineering methods for Bosch products that require multi-disciplinary collaboration of engineers and software developers. In this inspiring environment he focuses on improving programming and software engineering for deeply embedded resource-constraint real-time systems. In his current project his team develops a programming language in this area, with the intention to promote modern implementation technologies and to make embedded programming "attractive" for software professionals.

- Web page: https://www.linkedin.com/in/franzjosefg/

FDL 2018 is in Munich, Germany