×

zbMATH — the first resource for mathematics

A deadlock-free semantics for shared memory concurrency. (English) Zbl 1250.68207
Leucker, Martin (ed.) et al., Theoretical aspects of computing – ICTAC 2009. 6th international colloquium, Kuala Lumpur, Malaysia, August 16–20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03465-7/pbk). Lecture Notes in Computer Science 5684, 140-154 (2009).
Summary: We design a deadlock-free semantics for a concurrent, functional and imperative programming language where locks are implicitly and univocally associated with pointers. The semantics avoids unsafe states by relying on a static analysis of programs, by means of a type and effect system. The system uses singleton reference types, which allow us to have a precise information about the pointers that are anticipated to be locked by an expression.
For the entire collection see [Zbl 1169.68004].

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
Software:
Autolocker; Ynot
PDF BibTeX XML Cite
Full Text: DOI