Sciweavers

Share
OOPSLA
2010
Springer

Composable specifications for structured shared-memory communication

8 years 8 months ago
Composable specifications for structured shared-memory communication
In this paper we propose a communication-centric approach to specifying and checking how multithreaded programs use shared memory to perform inter-thread communication. Our approach complements past efforts for improving the safety of multithreaded programs such as race detection and atomicity checking. Unlike prior work, we focus on what pieces of code are allowed to communicate with one another, as opposed to declaring what data items are shared or what code blocks should be atomic. We develop a language that supports composable specifications at multiple levels of abstraction and that allows libraries to specify whether or not shared-memory communication is exposed to clients. The precise meaning of a specification is given with a formal semantics we present. We have developed a dynamic-analysis tool for Java that observes program execution to see if it obeys a specification. We report results for using the tool on several benchmark programs to which we added specifications, conclu...
Benjamin P. Wood, Adrian Sampson, Luis Ceze, Dan G
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where OOPSLA
Authors Benjamin P. Wood, Adrian Sampson, Luis Ceze, Dan Grossman
Comments (0)
books