Abstract semantic diffing of evolving concurrent programs

We present an approach for comparing two closely related concurrent programs, whose goal is to give feedback about interesting differences without relying on user-provided assertions. This approach compares two programs in terms of cross-thread interferences and data-flow, under a parametrized abstr...

Full description

Saved in:
Bibliographic Details
Published in:Formal methods in system design 2019-08, Vol.54 (1), p.4-26
Main Authors: Bouajjani, Ahmed, Enea, Constantin, Lahiri, Shuvendu K.
Format: Article
Language:English
Subjects:
CAE) and Design
Circuits and Systems
Computer-Aided Engineering (CAD
Concurrency
Electrical Engineering
Engineering
Semantics
Software Engineering/Programming and Operating Systems
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present an approach for comparing two closely related concurrent programs, whose goal is to give feedback about interesting differences without relying on user-provided assertions. This approach compares two programs in terms of cross-thread interferences and data-flow, under a parametrized abstraction which can detect any difference in the limit. We introduce a partial order relation between these abstractions such that a program change that leads to a “smaller” abstraction is more likely to be regression-free from the perspective of concurrency. On the other hand, incomparable or bigger abstractions, which are an indication of introducing new, possibly undesired, behaviors, lead to succinct explanations of the semantic differences.
ISSN:0925-9856
1572-8102
DOI:10.1007/s10703-018-0322-2