TY - GEN
T1 - Monitoring refinement via symbolic reasoning
AU - Emmi, Michael
AU - Enea, Constantin
AU - Hamza, Jad
N1 - Publisher Copyright:
© 2015 ACM.
PY - 2015/6/3
Y1 - 2015/6/3
N2 - Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations - or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations. We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violationdetection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions.
AB - Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between concurrent object invocations, one risks the conformance to reference implementations - or in formal terms, one risks violating observational refinement. Precisely testing this refinement even within a single execution is intractable, limiting existing approaches to executions with very few object invocations. We develop scalable and effective algorithms for detecting refinement violations. Our algorithms are founded on incremental, symbolic reasoning, and exploit foundational insights into the refinement-checking problem. Our approach is sound, in that we detect only actual violations, and scales far beyond existing violationdetection algorithms. Empirically, we find that our approach is practically complete, in that we detect the violations arising in actual executions.
KW - Concurrency
KW - Linearizability
KW - Refinement
U2 - 10.1145/2737924.2737983
DO - 10.1145/2737924.2737983
M3 - Conference contribution
AN - SCOPUS:84951767881
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 260
EP - 269
BT - PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - Blackburn, Steve
A2 - Grove, David
PB - Association for Computing Machinery
T2 - 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015
Y2 - 13 June 2015 through 17 June 2015
ER -