Towards type-theoretic semantics for transactional concurrency
Towards type-theoretic semantics for transactional concurrency
复制标题
面向事务并发的类型论语义
DOI：
10.1145/1481861.1481872
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Greg Morrisett
中科院分区：
文献类型：
--
作者：
Aleksandar Nanevski;Paul Govereau;Greg Morrisett
我们提出了一个依赖类型理论，集成编程，规范和推理高阶并发程序共享事务内存。该设计建立在我们以前对Hoare类型理论（HTT）的工作基础上，我们扩展了与Hoare风格的事务规范相对应的类型。这些类型分别跟踪进程的共享状态和本地状态，并强制共享状态总是满足给定的不变量，除了在特定的临界区，这些临界区似乎是原子执行的。原子部分可能会违反不变量，但必须在退出时恢复它。HTT遵循分离逻辑，提供严格的空间要求规范。
作为一个逻辑，我们认为，HTT是健全的和组成。作为一种编程语言，我们定义了它的操作语义，并显示充分的规范。
We propose a dependent type theory that integrates programming, specifications, and reasoning about higher-order concurrent programs with shared transactional memory. The design builds upon our previous work on Hoare Type Theory (HTT), which we extend with types that correspond to Hoare-style specifications for transactions. The types track shared and local state of the process separately, and enforce that shared state always satisfies a given invariant, except at specific critical sections which appear to execute atomically. Atomic sections may violate the invariant, but must restore it upon exit. HTT follows Separation Logic in providing tight specifications of space requirements.
As a logic, we argue that HTT is sound and compositional. As a programming language, we define its operational semantics and show adequacy with respect to specifications.
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds