Skip to end of metadata
Go to start of metadata

You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 16 Next »

PRETSY - Precision-Timed Synchronous Reactive Processing

The PRETSY project is a project funded by the German Research Foundation (DFG HA 4407/6-1), running 2011 - 2014.

Summary:

Embedded reactive real-time systems are ubiquitous today, and provide increasingly complex functionality for example in modern automotive, avionics or medical products. This rising complexity makes it important to apply high-level design approaches, which, however, traditionally make critical low-level aspects such as timing hard to control. This project will investigate a novel, holistic approach for the design of timing-predictable, efficient reactive systems, which considers the modeling and programming level as well as the execution platform.

A key contribution will be to combine a formal semantical basis, which is provided by the synchronous model of computation and which results in predictable reactive control flow, with recent architectural developments that offer predictable timing at the instruction level. Compared to typical design approaches today, based on C-like languages and processors that optimize the average case at the expense of predictability, this will reduce timing uncertainties at the control-flow level as well as the architectural level. On the practical side the project will develop a model-based design flow and tool chain for implementing timing-predictable, reactive systems, including a synchronous modeling and programming language, a compiler, a timing analyzer, and a predictable execution platform derived from the Berkeley/Columbia PRET architecture.

Coordinators:

Reinhard v. Hanxleden, Kiel University

Michael Mendler, Bamberg University

Collaborating Scientists:

Stephen Edwards, Columbia University

Alain Girault, INRIA Grenoble

Edward Lee, UC Berkeley

Gerald Lüttgen, Bamberg University

Marc Pouzet, ENS Paris

Partha Roop, University of Auckland

Zoran Salcic, University of Auckland

Reinhard Wilhelm, Saarland University

Internal Documents:

Internal Documents

Mailinglists:

If you wish to receive important project updates and announcements in low-traffic mode, this mailing list is just for you:

pretsy mailinglist

Active group members and developers should subscribe to:

pretsy-devel mailinglist


Papers:

[DATE’13]

Sequentially Constructive Concurrency: A Conservative Extension of the Synchronous Model of Computation.

R. von Hanxleden, M. Mendler, J. Aguado, B. Duderstadt, I. Fuhrmann, C. Motika, S. Mercer, O. O'Brian

Design, Automation Test in Europe Conference (DATE’13), March 2013: 581-586.

Abstract. Synchronous languages ensure deterministic concurrency, but at the price of heavy restrictions on what programs are considered valid, or constructive. Meanwhile, sequential languages such as C and Java offer an intuitive, familiar programming paradigm but provide no guarantees with regard to deterministic concurrency. The sequentially constructive (SC) model of computation (MoC) presented here harnesses the synchronous execution model to achieve deterministic concurrency while addressing concerns that synchronous languages are unnecessarily restrictive and difficult to adopt.

In essence, the SC MoC extends the classical synchronous MoC by allowing variables to be read and written in any order as long as sequentiality expressed in the program provides sufficient scheduling information to rule out race conditions. This allows to use programming patterns familiar from sequential programming, such as testing and later setting the value of a variable, which are forbidden in the standard synchronous MoC. The SC MoC is a conservative extension in that programs considered constructive in the common synchronous MoC are also SC and retain the same semantics. In this paper, we investigate classes of shared variable accesses, define SC admissible scheduling as a restriction of "free scheduling," derive the concept of sequential constructiveness, and present a priority-based scheduling algorithm for analyzing and compiling SC programs efficiently.

 

[CSIJC’13]

A Game Semantics for Instantaneous Esterel Reactions.

J. Aguado

CSI Journal of Computing (CSIJC). Vol.2, No.1-2, e-ISSN 2277-7091, 2013: 30-44.

Abstract. The present paper explains the constructive semantics of the synchronous language Estterel in terms of winning strategies in finite two–player games. The kernel fragment of Esterel considered here corresponds to combinational circuits and includes the statements for signal emission, status test, parallel composition and gives for the first time a game–theoretic interpretation to sequential composition and local signal declaration. This modelling shows how non-classical truth values induced by logic games can be used to characterise the constructive single-step semantics for Esterel.

 

[ESOP’14]

Grounding Synchronous Deterministic Concurrency in Sequential Programming.

J. AguadoM. MendlerR. von HanxledenI. Fuhrmann.

Proceedings of the 23rd European Symposium on Programming (ESOP'14), April 2014: 229-248.

Abstract. Using a new domain-theoretic characterisation we show that Berry’s constructive semantics is a conservative approximation of the recently proposed sequentially constructive (SC) model of computation. We prove that every Berry-constructive program is deterministic and deadlock-free under sequentially admissible scheduling. This gives, for the first time, a natural interpretation of Berry-constructiveness for shared-memory, multi-threaded programming in terms of synchronous cycle-based scheduling, where previous results were cast in terms of synchronous circuits. This opens the door to a direct mapping of Esterel’s signal mechanism into Boolean variables that can be set and reset under the programmer’s control within a tick. We illustrate the practical usefulness of this mapping by discussing how signal reincarnation is handled efficiently by this transformation, which is of linear complexity in program size, in contrast to earlier techniques that had quadratic overhead.

 

[PLDI’14]

SCCharts: Sequentially Constructive Statecharts for Safety-Critical Applications (HW/SW-Synthesis for a Conservative Extension of Synchronous Statecharts).

R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer, O. O'Brian

ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14), June 2014.

Abstract. We present a new visual language, SCCharts, designed for specifying safety-critical reactive systems. SCCharts use a statechart notation and provide determinate concurrency based on a synchronous model of computation (MoC), without restrictions common to previous synchronous MoCs. Specifically, we lift earlier limitations on sequential accesses to shared variables, by leveraging the sequentially constructive MoC. The semantics and key features of SCCharts are defined by a very small set of elements, the Core SCCharts, consisting of state machines plus fork/join concurrency. We also present a compilation chain that allows efficient synthesis of software and hardware.

 

[TECS’14]

Sequentially Constructive Concurrency—A Conservative Extension of the Synchronous Model of Computation.

R. von Hanxleden, M. Mendler, J. Aguado, B. Duderstadt, I. Fuhrmann, C. Motika, S. Mercer, O. O'Brian, P. Roop.  

ACM Transactions on Embedded Computing Systems (ACM TECS) - Special Issue on Applications of Concurrency to System Design, to appear 2014.

Abstract. This is a journal extended version of [DATE’13] which includes in addition ...


Workshops/Seminars:

[PTCONF’13]

Sequentially Constructive Charts (SCCharts)

C. Motika, S. Smyth, R. von Hanxleden, M. Mendler.

10th Biennial Ptolemy Miniconference (PTCONF’13), Berkeley, CA, USA, November 2013.

Summary: Poster.

 

[SYNCHRON’13-1]

Compiling SCCharts (and other Sequentially Constructive Programs) to Hardware and Software.

R. von Hanxleden.

20th International Workshop on Synchronous Programming (SYNCHRON'13), Dagstuhl Germany, November 2013.

Summary: SCCharts extend SyncCharts with sequential constructiveness (SC) and other features. We developed a compilation chain that first, in a high-level compilation phase, performs a sequence of model-to-model transformations at the SCCharts-level such that they can be mapped directly to SC Graphs (SCGs). Then two alternative low-level compilation approaches allow mapping to hardware and software; the circuit approach generates a netlist, the priority approach simulates concurrency with interleaved threads.

 

[SYNCHRON’13-2]

SCCharts – Sequentially Constructive Charts. (slides)

C. Motika

20th International Workshop on Synchronous Programming (SYNCHRON'13), Dagstuhl Germany, November 2013.

Summary: We present a new visual language, SCCharts, designed for specifying safety-critical reactive systems. SCCharts uses a new statechart notation similar to Harel Statecharts and provides deterministic concurrency based on a synchronous model of computation (MoC), without restrictions common to previous synchronous MoCs like the Esterel constructive semantics. Specifically, we lift earlier limitations on sequential accesses to shared variables, by leveraging the sequentially constructive MoC. Thus SCCharts in short are SyncCharts syntax plus Sequentially Constructive semantics.

The key features of SCCharts are defined by a very small set of elements, the Core SCCharts, consisting of state machines plus fork/join concurrency. Conversely, Extended SCCharts contain a rich set of advanced features, such as different abort types, signals, history transitions, etc., all of which can be reduced via semantics preserving model-to-model (M2M) transformations into Core SCCharts. Extended SCCharts features are syntactic sugar because they can be expressed by a combination of Core SCCharts features.

On the one hand this eases the compilation and makes it more robust because it reduces its complexity. On the other hand, using Extended SCCharts features, a modeler is able to abstract away complexity of his or her SCCharts model which increases robustness and readability of a model. This approach enables a simple yet efficient compilation strategy and aids verification and certification.

 

Recently Updated

 
Navigate space
  • No labels