enter search term and/or author name
Semantics of transactional memory and automatic mutual exclusion
Martín Abadi, Andrew Birrell, Tim Harris, Michael Isard
Article No.: 2
Software Transactional Memory (STM) is an attractive basis for the development of language features for concurrent programming. However, the semantics of these features can be delicate and problematic. In this article we explore the trade-offs...
Locksmith is a static analysis tool for automatically detecting data races in C programs. In this article, we describe each of Locksmith's component analyses precisely, and present systematic measurements that isolate interesting trade-offs...
Mechanically verified proof obligations for linearizability
John Derrick, Gerhard Schellhorn, Heike Wehrheim
Article No.: 4
Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed linearizability as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent...
Environmental bisimulations for higher-order languages
Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
Article No.: 5
Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, as well as enhancements of the bisimulation proof method with “up-to context” techniques, and (2)...