Child pages
  • Home

Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

pretsy-devel mailinglist

 

...

Papers:

[FMSD’12] Constructive Boolean circuits and the exactness of timed ternary simulation.

...

As the corner-stone of our main results we introduce UN-Logic, an axiomatic specification language for UN-delay circuits that mediates between the real-time behavior and its abstract simulation in the ternary domain. We present a symbolic simulation 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 correctness and exactness result for the timing analysis of cyclic circuits. Our algorithm is a timed extension of Malik’s pure ternary algorithm and closely related to the timed algorithm proposed by Riedel and Bruck, which however was not formally linked with real-time execution models.

 

[DATE’13] Sequentially Constructive Concurrency: A Conservative Extension of the Synchronous Model of Computation. (slides)

...

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. (pdf)

...

Abstract. The present paper explains the constructive semantics of the synchronous language Esterel 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 emission, signal 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. (slides)

...

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).

...

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.

...

Summary: Synchronous programs 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 talk, we study the problem of static worst case reaction (WCRT) time analysis of synchronous programs. While, there have been many recent attempts at addressing this problem from the point of view of scalability and precision, one crucial aspect is yet to be examined from a fundamental viewpoint. Concurrent threads in a synchronous program must align during every reaction, a problem that has been termed as the tick alignment problem (TAP), i.e., infeasible 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 formulation in order to not only explore its lower bound complexity, but also to develop heuristics that work well in practice.

 

...

Technical Reports:

[TR1308] Sequentially Constructive Concurrency. A Conservative Extension of the Synchronous Model of Computation. (pdf)

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

Technical Report 1308, Christian-Albrechts-Universitaet zu Kiel, Department of Computer Science,  ISSN 2192-6247, August 2013

 

 

Section
Column
width60%
Recently Updated
Column
width2%
 
Column
width38%
Navigate space
Page Tree Search
Page Tree