A Memory-Bounded, Deterministic and Terminating Semantics for the Synchronous Programming Language CEU

被引：0

作者：

Santos, Rodrigo C. M. ^{[1
]}

Lima, Guilherme F. ^{[1
]}

Sant'Anna, Francisco ^{[2
]}

Ierusalimschy, Roberto ^{[1
]}

Haeusler, Edward H. ^{[1
]}

机构：

[1] Pontificia Univ Catolica Rio de Janeiro, Rio de Janeiro, RJ, Brazil

[2] Univ Estado Rio De Janeiro, Rio De Janeiro, RJ, Brazil

来源：

ACM SIGPLAN NOTICES | 2018年 / 53卷 / 06期

关键词：

Determinism; Termination; Operational semantics; Synchronous languages;

D O I：

10.1145/3211332.3211334

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

CEU is a synchronous programming language for embedded soft real-time systems. It focuses on control-flow safety features, such as safe shared-memory concurrency and safe abortion of lines of execution, while enforcing memory-bounded, deterministic, and terminating reactions to the environment. In this work, we present a small-step structural operational semantics for CEU and a proof that reactions have the properties enumerated above: that for a given arbitrary timeline of input events, multiple executions of the same program always react in bounded time and arrive at the same final finite memory state.

引用

页码：1 / 18

页数：18