Date: Tue, 19 Mar 2024 09:35:20 +0000 (UTC) Message-ID: <819222317.6067.1710840920312@2f9704fbf185> Subject: Exported From Confluence MIME-Version: 1.0 Content-Type: multipart/related; boundary="----=_Part_6066_1588300210.1710840920311" ------=_Part_6066_1588300210.1710840920311 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Content-Location: file:///C:/exported.html
The PRETSY project is a= project funded by the German Research Foundation (DFG HA 4407/6-1, ME 1427= /6-1), running 2012 - 2015 and 2015 - 2018.
Embedded reactive real-=
time systems are ubiquitous today, and provide increasingly complex functio=
nality 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 tim=
ing hard to control. This project investigates a novel, holistic approach f=
or the design of timing-predictable, efficient reactive systems, which cons=
iders the modelling and programming level as well as the execution platform=
.
A key aim is to combine a formal semantical basis, which is provid=
ed by the synchronous model of computation and which results in predictable=
reactive control flow, with recent architectural developments that offer p=
redictable timing at the instruction level. Compared to typical design appr=
oaches today, based on C-like languages and processors that optimise the av=
erage case at the expense of predictability, the objective is to reduce tim=
ing uncertainties at the control-flow level as well as the architectural le=
vel. On the practical side the project is developing a model-based design f=
low and tool chain for implementing timing-predictable, reactive systems, i=
ncluding a synchronous modelling and programming language, a compiler, a ti=
ming analyser, and a predictable execution platform derived from the Berkel=
ey/Columbia PRET architecture.
PRETSY (p= oster)
Reinhard v. Hanxleden, = Kiel University
Michael Mendler, Bamber= g University
Stephen Edwards, Columb= ia University
Alain Girault, INRIA Gr= enoble
Edward Lee, UC Berkeley=
Gerald L=C3=BCttgen, Ba= mberg University
Marc Pouzet, ENS Paris<= /p>
Partha Roop, University= of Auckland
Zoran Salcic, Universit= y of Auckland
Reinhard Wilhelm, Saarl= and University
If you wish to receive important project updates and announcements in lo= w-traffic mode, this mailing list is just for you:
Active group members and developers should subscribe to:
[FMSD=E2=80=9912] Constructive Boolean circuits and the exactnes= s of timed ternary simulation.
M. Mendler, T. R. Shiple, G. Berry.
Formal Methods in System Design (FMSD), Volume 40, = Issue 3, June 2012: 283-329.
Abstract. We classify gate level circuits with cycles based on their stabiliz= ation behavior. We define a formal class of combinational circuits, the constructive circuits, for which signals settle to a unique value in = bounded time, for any input, under a simple conservative delay model, calle= d the up-bounded non-inertial (UN) delay. Since circuits with comb= inational cycles can exhibit asynchronous behavior, such as non-determinism= or metastability, it is crucial to ground their analysis in a formal delay= model, which previous work in this area did not do.
We prove that t= ernary simulation, such as the practical algorithm proposed by Malik, = decides the class of constructive circuits. We prove that three-va= lued algebra is able to maintain correct and exact stabilization informatio= n under the UN-delay model, and thus provides an adequate electrical interp= retation of Malik=E2=80=99s algorithm, which has been missing in the litera= ture. Previous work on combinational circuits used the upbounded inerti= al (UI) delay to justify ternary simulation. We show that the match is= not exact and that stabilization under the UI-model, in general, cannot be= decided by ternary simulation. We argue for the superiority of the UN-mode= l for reasons of complexity, compositionality and electrical adequacy. The = UN-model, in contrast to the UI-model, is consistent with the hypothesis th= at physical mechanisms cannot implement non-deterministic choice in bounded= time.
As the corner-stone= of our main results we introduce UN-Logic, an axiomatic specifica= tion language for UN-delay circuits that mediates between the real-time beh= avior and its abstract simulation in the ternary domain. We present a symbo= lic simulation calculus for circuit theories expressed in UN-logic and prov= e it sound and complete for the UN-model. This provides, for the first time= , a correctness and exactness result for the timing analysis of cyclic circ= uits. Our algorithm is a timed extension of Malik=E2=80=99s pure ternary al= gorithm and closely related to the timed algorithm proposed by Riedel and B= ruck, which however was not formally linked with real-time execution models= .
[DATE=E2=80=9913] Sequentially Constructive Concurrency: A Conse= rvative Extension of the Synchronous Model of Computation. (slides)
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=E2= =80=9913), March 2013: 581-586.
Abstract. Synchronous la= nguages ensure deterministic concurrency, but at the price of heavy restric= tions on what programs are considered valid, or constructive. Meanwhile, se= quential languages such as C and Java offer an intuitive, familiar programm= ing paradigm but provide no guarantees with regard to deterministic concurr= ency. The sequentially constructive (SC) model of computation (MoC) present= ed here harnesses the synchronous execution model to achieve deterministic = concurrency while addressing concerns that synchronous languages are unnece= ssarily restrictive and difficult to adopt.
In essence, the SC MoC extends the classi= cal synchronous MoC by allowing variables to be read and written in any ord= er as long as sequentiality expressed in the program provides sufficient sc= heduling information to rule out race conditions. This allows to use progra= mming patterns familiar from sequential programming, such as testing and la= ter setting the value of a variable, which are forbidden in the standard sy= nchronous MoC. The SC MoC is a conservative extension in that programs cons= idered constructive in the common synchronous MoC are also SC and retain th= e same semantics. In this paper, we investigate classes of shared variable = accesses, define SC admissible scheduling as a restriction of "free schedul= ing," derive the concept of sequential constructiveness, and present a prio= rity-based scheduling algorithm for analyzing and compiling SC programs eff= iciently.
[CSIJC=E2=80=9913] A Game Semantics for Instantaneous Esterel Re= actions. (pdf)
J. Aguado.
CSI Journal of Computing (CSIJC).= Vol.2, No.1-2, e-ISSN 2277-7091, 2013: 30-44.
Abstract. The present pa= per explains the constructive semantics of the synchronous language Esterel= in terms of winning strategies in finite two=E2=80=93player games. The ker= nel fragment of Esterel considered here corresponds to combinational circui= ts and includes the statements for emission, signal test, parallel composit= ion and gives for the first time a game=E2=80=93theoretic interpretation to= sequential composition and local signal declaration. This modelling shows = how non-classical truth values induced by logic games can be used to charac= terise the constructive single-step semantics for Esterel.
[ESOP=E2=80=9914] Grounding Synchronous Deterministic Concurrenc= y in Sequential Programming. (slides= )
J. Aguado, M. Mendler, R. von Hanxleden, I. Fuhrmann.
Proceedings of the 23rd European Symposium on Programming (ESOP'14), April 2014: 229-248.
Abstract. Using a new do= main-theoretic characterisation we show that Berry=E2=80=99s constructive s= emantics is a conservative approximation of the recently proposed seque= ntially constructive (SC) model of computation. We prove that every Be= rry-constructive program is deterministic and deadlock-free under sequentia= lly admissible scheduling. This gives, for the first time, a natural interp= retation of Berry-constructiveness for shared-memory, multi-threaded progra= mming in terms of synchronous cycle-based scheduling, where previous result= s were cast in terms of synchronous circuits. This opens the door to a dire= ct mapping of Esterel=E2=80=99s signal mechanism into Boolean variables tha= t can be set and reset under the programmer=E2=80=99s 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 tec= hniques that had quadratic overhead.
[PLDI=E2=80=9914] SCCharts: Sequentially Constructive Statechart= s for Safety-Critical Applications: HW/SW-Synthesis for a Conservative Exte= nsion 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=E2=80=9914), June 2014.
Abstract. We present a n= ew visual language, SCCharts, designed for specifying safety-critical react= ive systems. SCCharts use a statechart notation and provide determinate con= currency based on a synchronous model of computation (MoC), without restric= tions common to previous synchronous MoCs. Specifically, we lift earlier li= mitations on sequential accesses to shared variables, by leveraging the seq= uentially constructive MoC. The semantics and key features of SCCharts are = defined by a very small set of elements, the Core SCCharts, consisting of s= tate machines plus fork/join concurrency. We also present a compilation cha= in that allows efficient synthesis of software and hardware.
[TECS=E2=80=9914] Sequentially Constructive Concurrency =E2=80= =94 A Conservative Extension of the Synchronous Model of Computation.
R. von Hanxleden, M. Mendler, J. Ag= uado, B. Duderstadt, I. Fuhrmann, C. Motika, S. Mercer, O. O'Brian, P. Roop= .
ACM Transactions on Embedded Computing Systems (ACM TECS= ) =E2=80=94 Special Issue on Applications of Concurrency to System Des= ign, Vol. 13, Issue 4s, June 2014: 144:1-144:26
Abstract. This is a jour= nal extended version of the [DATE=E2=80=9913] publication which includes in= addition: (i) a description of the mapping from the Sequentially Construct= ive (SC) language to the SC graph (SCG); (ii) detailed discussions on threa= d and statement reincarnation; (iii) a full section on the formalisation of= SC based on free scheduling of SCGs; (iv) a more general SC Model of Compu= tation based on the notion of confluence; (v) a revised (positive) de= finition of SC-Admissibility; (vi) definition of valid SC-schedules; (vii) = proof that every ASC schedulable program is indeed SC; (viii) detailed disc= ussion on conservative approximations and (ix) additional examples for illu= strating ineffective writes, failure despite deterministic outcome, data-de= pendency of SC and enforced determinism via reduction of admissible runs.= p>
[ISoLA'14] Compiling SCCharts =E2=80=94 a case-study o= n interactive model-based compilation.
C. Motika, S. Smyth, and R. von Hanxleden.
Proceedings of the 6th International Symposium on Leveraging Application= s of Formal Methods, Verication and Validation, LNCS 8802, October 2014: 44= 3-462.
Abstract. SCCharts is a = recently proposed statechart language designed for specifying safety-critic= al reactive systems. We have developed an Eclipse-based compilation chain t= hat synthesizes SCCharts into either hardware or software. The user edits a= textual description which is visualized as SCChart and subsequently transf= ormed into VHDL or C code via a series of model-to-model (M2M) transformati= on steps. An interactive environment gives the user control over which tran= sformations are applied and allows the user to inspect intermediate transfo= rmation results. This Single-Pass Language-Driven Incremental Compilati= on (SLIC) approach should conceptually be applicable to other language= s as well. Key benets are: (1) a compact, light-weight denition of the core= semantics, (2) intermediate transformation results open to inspection and = support for certication, (3) high-level formulations of transformations tha= t define advanced language constructs, (4) a divide-and-conquer validation = strategy, (5) simplied language/compiler subsetting and DSL construction.= p>
[SYNCHRON=E2=80=9912] Sequentially Constructive Concurrency: A C= onservative Extension of the Synchronous Model of Computation. (slides)
M. Mendler.
Summary: Presentatio= ns of the [DATE=E2=80=9913] and [TECS=E2=80=9914] publications respectively= .
Also presented at
[PDAY=E2=80=9913<= /a>] Is timing analysis a refinement of causality analysis? (slides)
J. Aguado.
PRET Day, Inria Grenoble Rh=C3=B4ne-Alpes France, March 2013.
Summary: It has been rec= ognised that the synchronous model of computation together with a suitable = execution platform (precision-timed, or PRET architectures) facilitates sys= tem-level timing predictability. This talk discusses a logical and game-the= oretic framework for capturing worst-case reaction time (WCRT) for Esterel-= style synchronous reactive programming. This framework will provide a forma= l grounding for the WCRT problem, and allow to improving upon earlier heuri= stics by accurately and modularly characterising timing interfaces. This ap= proach will not only allows verifying the correctness of WCRT analyses meth= ods, but also will allow capturing functionality and timing together.
[PDAY=E2=80=991= 3] Constructive Boole= an Networks and the Exactness of Timed Ternary Simulation. = (slides)
M. Mendler.
Summary: Presentations o= f materials included in the [FMSD=E2=80=9912] publication.
Cyclic boolean systems, such as those ari= sing in asynchronous circuits the semantics of synchronous programming lang= uages, do not admit a unique canonical execution semantics. Instead, differ= ent approaches impose different restrictions on their stabilization behavio= r. This talk concerns the class of constructive circuits, for which signals= settle to a unique value in bounded time, for any input, under a simple co= nservative delay model, called the up-bounded non-inertial (UN) delay. The = main result is that ternary simulation decides the class of constructive ci= rcuits. It shows that three-valued algebra is able to maintain correct and = exact stabilization information under the UN-delay model, which thus provid= es an adequate electrical interpretation of ternary algebra, which has been= missing in the literature. Previous work on combinational circuits used th= e up-bounded inertial (UI) delay to justify ternary simulation. It can be s= hown that the match is not exact and that stabilization under the UI-model,= in general, cannot be decided by ternary simulation. As the corner-stone o= f our main results we introduce UN-Logic, an axiomatic specification langua= ge for UN-delay circuits that mediates between the real-time behavior and i= ts abstract simulation in the ternary domain. We present a symbolic simulat= ion calculus for circuit theories expressed in UN-logic and prove it sound = and complete for the UN-model. This provides, for the first time, a correct= ness and exactness result for the timing analysis of cyclic circuits such a= s the timed extension of Malik's or Brzozowski and Seger's pure ternary alg= orithm or the timed algorithm proposed by Riedel and Bruck, which were not = formally linked with real-time execution models.
Also presented at:
[PTCONF=E2=80=9913] SCCharts: Sequentially Constructive Charts.<= /strong> (pos= ter)
C. Motika, S. Smyth, R. von Hanxleden, M. Mendler.
10th Biennial Ptolemy Miniconference (PTCONF= =E2=80=9913), Berkeley, CA, USA, November 2013.
Summary: This poster des= cribes Sequentially Constructive Charts (SCCharts), the visual language for= specifying safety-critical reactive systems employed in the [PLDI=E2=80=99= 14] publication.
[SYNCHRON=E2=80=9913] 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 201= 3.
Summary: SCCharts extend= SyncCharts with sequential constructiveness (SC) and other features. We de= veloped 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 altern= ative low-level compilation approaches allow mapping to hardware and softwa= re; the circuit approach generates a netlist, the priority approach simulat= es concurrency with interleaved threads.
[SYNCHRON=E2=80=9913] SCCharts =E2=80=93 Sequentially Constructi= ve Charts. (slides)
C. Motika.
20th International Workshop on Synchronous Programming (SYNCHRON'13), Dagstuhl Germany, November 201= 3.
Summary: We present a ne= w visual language, SCCharts, designed for specifying safety-critical reacti= ve systems. SCCharts uses a new statechart notation similar to Harel Statec= harts and provides deterministic concurrency based on a synchronous model o= f computation (MoC), without restrictions common to previous synchronous Mo= Cs like the Esterel constructive semantics. Specifically, we lift earlier l= imitations on sequential accesses to shared variables, by leveraging the se= quentially constructive MoC. Thus SCCharts in short are SyncCharts syntax p= lus Sequentially Constructive semantics.
The key features of SCCharts are defined = by a very small set of elements, the Core SCCharts, consisting of state mac= hines plus fork/join concurrency. Conversely, Extended SCCharts contain a r= ich set of advanced features, such as different abort types, signals, histo= ry 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 compilatio= n 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 read= ability of a model. This approach enables a simple yet efficient compilatio= n strategy and aids verification and certification.
[SYNCHRON=E2=80=9913] Berry-Constructive Programs are Sequential= ly Constructive, or: Synchronous Programming from a Scheduling Perspective.= (slides)
M. Mendler.
20th International Workshop on Synchronous Programming (SYNCHRON'13), Dagstuhl Germany, November 201= 3.
Summary: We introduce an= abstract value domain I(D) and associated fixed point semantics for reason= ing about concurrent and sequential variable valuations within a synchronou= s cycle-based model of computation. We use this domain for a new behavioura= l definition of Berry=E2=80=99s causality analysis for Esterel in terms of = approximation intervals. This gives a compact and more uniform understandin= g of causality and generalises to other data-types. We also prove that Este= rel=E2=80=99s ternary domain and its semantics is conservatively extended b= y the recently proposed sequentially constructive (SC) model of computation= . This opens the door to a direct mapping of Esterel=E2=80=99s signal mecha= nism into boolean variables that can be set and reset arbitrarily within a = tick. We illustrate the practical usefulness of this mapping by discussing = how signal reincarnation is handled efficiently by this transformation, whi= ch is of complexity that is linear in program size, in contrast to earlier = techniques that had, at best, potentially quadratic overhead.
[RePP=E2=80=9914] Towards Interactive Timing Analysis for Design= ing Reactive Systems. (slides)
I. Fuhrmann (talk), David Broman, Steven Smyth, Reinhard von Hanxled=
en.
Workshop on Reconciling Performance with Predictability (RePP=E2=80=99= 14), Grenoble France, April 2014.
Summary: Reactive system= s are increasingly developed using high-level modeling tools. Such modeling= tools may facilitate formal reasoning about concurrent programs, but provi= de little help when timing-related problems arise and deadlines are missed = when running a real system. In these cases, the modeler has typically no in= formation about timing properties and costly parts of the model; there is l= ittle or no guidance on how to improve the timing characteristics of the mo= del. Here, we propose a design methodology where interactive timing analysi= s is an integral part of the modeling process. This methodology concerns ho= w to aggregate timing values in a user-friendly manner and how to define ti= ming analysis requests. We also introduce and formalize a new timing analys= is interface that is designed for communicating timing information between = a high-level modeling tool and a lower-level timing analysis tool.
[RePP=E2=80=9914] Worst Case Reaction Time analysis of Sync= hronous Programs: Studying the Tick Alignment Problem. (slides)
M. Mendler.
Workshop on Reconciling Performance with Predictability (RePP=E2=80=99= 14), Grenoble France, April 2014.
Summary: Synchronous pro= grams are ideally suited for the design of safety critical systems as they = provide guarantees on determinism and deadlock freedom. In addition to such= functional guarantees, guarantees on timing are also necessary. In this ta= lk, we study the problem of static worst case reaction (WCRT) time analysis= of synchronous programs. While, there have been many recent attempts at ad= dressing this problem from the point of view of scalability and precision, = one crucial aspect is yet to be examined from a fundamental viewpoint. Conc= urrent threads in a synchronous program must align during every reaction, a= problem that has been termed as the tick alignment problem (TAP), i.e., in= feasible ticks that never align in practice must be ruled out for precision= . We, for the first time, study TAP in the guise of a number theoretic form= ulation in order to not only explore its lower bound complexity, but also t= o develop heuristics that work well in practice.
[TR1308] Sequentially Constructive Concurrency. A Conservative E=
xtension of the Synchronous Model of Computation. (pdf)
R. von Hanxleden, M. Mendler, J. Aguado, B. Duderstadt, I. Fuhrmann,= C. Motika, S. Mercer, O. O=E2=80=99Brien, P. Roop.
Technical Report 1308, Christian-Albrechts-Universitaet zu Kiel, Departm= ent of Computer Science, ISSN 2192-6247, August 2013.
[TR1311] SCCharts: Sequentially Constructive Statecharts for Saf= ety-Critical Applications. (pdf)
R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J.= Aguado, S. Mercer, and O. O=E2=80=99Brien.
Technical Report 1311, Christian-Albrechts-Universitaet zu Kiel, Departm= ent of Computer Science, ISSN 2192-6247 December 2013.
[EECS-14-26] Towards Interactive Timing Analysis for Designing R= eactive Systems. (pdf)
I. Fuhrmann, D. Broman, S. Smyth, R. von Hanxleden.
Technical Report No. UCB/EECS-2014-26, University of California, Berkele= y, EECS Department, April 2014.
[TR94] Grounding Synchronous Deterministic Concurrency in S=
equential Programming. (pdf)
J. Aguado, M. Mendler, R. von Hanxleden, I. Fuhrmann.
Bamberger Beitr=C3=A4ge zur Wirtschaftsinformatik und Angewandten Inform= atik Nr. 94, Bamberg University, ISSN 0937-3349, August 2014.
[TR95] WCRT analysis of Synchronous Programs: Studying the Tick =
Alignment Problem (pdf)
<=
/strong>
M. Mendler, B. Bodin, P. S. Roop, J.-J. Wang.
Bamberger Beitr=C3=A4ge zur Wirtschaftsinformatik und Angewandten Inform= atik Nr. 95, Bamberg University, ISSN 0937-3349, August 2014.