Syntactic control of concurrency |
| |
Authors: | DR Ghica AS Murawski C-HL Ong |
| |
Affiliation: | Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford OX1 3QD, UK |
| |
Abstract: | We consider a finitary procedural programming language (finite data-types, no recursion) extended with parallel composition and binary semaphores. Having first shown that may-equivalence of second-order open terms is undecidable we set out to find a framework in which decidability can be regained with minimum loss of expressivity. To that end we define an annotated type system that controls the number of concurrent threads created by terms and give a fully abstract game semantics for the notion of equivalence induced by typable terms and contexts. Finally, we show that the semantics of all typable terms, at any order and in the presence of iteration, has a regular-language representation and thus the restricted observational equivalence is decidable. |
| |
Keywords: | Game semantics Type systems Model checking |
本文献已被 ScienceDirect 等数据库收录! |
|