...
Abstract. This is a journal extended version of the [DATE’13] publication which includes in addition: (i) a description of the mapping from the Sequentially Constructive (SC) language to the SC graph (SCG); (ii) detailed discussions on thread 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 Computation based on the notion of confluence; (v) a revised (positive) definition of SC-Admissibility; (vi) definition of valid SC-schedules; (vii) proof that every ASC schedulable program is indeed SC; (viii) detailed discussion on conservative approximations and (ix) additional examples for illustrating ineffective writes, failure despite deterministic outcome, data-dependency of SC and enforced determinism via reduction of admissible runs.
...
Workshops/Seminars:
[PTCONF’13]
SCCharts: Sequentially Constructive Charts. (poster)
C. Motika, S. Smyth, R. von Hanxleden, M. Mendler.
10th Biennial Ptolemy Miniconference (PTCONF’13), Berkeley, CA, USA, November 2013.
Summary: Poster.
[PDAY’13-1]
Is timing analysis a refinement of causality analysis? (slides)
...
Summary: Cyclic boolean systems, such as those arising in asynchronous circuits the semantics of synchronous programming languages, do not admit a unique canonical execution semantics. Instead, different approaches impose different restrictions on their stabilization behavior. 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 conservative delay model, called the up-bounded non-inertial (UN) delay. The main result is that ternary simulation decides the class of constructive circuits. It shows that three-valued algebra is able to maintain correct and exact stabilization information under the UN-delay model, which thus provides an adequate electrical interpretation of ternary algebra, which has been missing in the literature. Previous work on combinational circuits used the up-bounded inertial (UI) delay to justify ternary simulation. It can be shown 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 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 such as the timed extension of Malik's or Brzozowski and Seger's pure ternary algorithm or the timed algorithm proposed by Riedel and Bruck, which were not formally linked with real-time execution models.
[PTCONF’13]
SCCharts: Sequentially Constructive Charts. (poster)
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.
...