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 perform inter-thread communication. Our complements past efforts for improving the safety of such as race detection atomicity checking. Unlike prior work, focus on what pieces code are allowed communicate with one another, opposed declaring data items or blocks should be atomic. We develop language that supports composable specifications at multiple levels abstraction allows libraries specify whether not shared-memory communication is exposed clients. The precise meaning specification given formal semantics present. have developed dynamic-analysis tool Java observes program execution see if it obeys specification. report results using several benchmark which added specifications, concluding our matches modular structure applications performant enough in development testing.