ACM DL

Programming Languages and Systems (TOPLAS)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 33 Issue 1, January 2011

Editorial
Jens Palsberg
Article No.: 1
DOI: 10.1145/1889997.1889998

Semantics of transactional memory and automatic mutual exclusion
Martín Abadi, Andrew Birrell, Tim Harris, Michael Isard
Article No.: 2
DOI: 10.1145/1889997.1889999

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: Practical static race detection for C
Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks
Article No.: 3
DOI: 10.1145/1889997.1890000

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
DOI: 10.1145/1889997.1890001

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
DOI: 10.1145/1889997.1890002

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)...