Decidable Race Condition and Open Coregions in HMSC

Abstract

Message Sequence Charts (MSCs) is a visual formalism for the description of
communication behaviour of distributed systems. An MSC specifies relations
between communication events with partial orders. A situation when two
visually ordered events may occur in any order during an execution of an MSC
is called a race and is usually considered as a design error. While there
is a quadratic time algorithm detecting races in a finite communication
behaviours called Basic Message Sequence Charts (BMSCs), the race detection
problem is undecidable for High-level Message Sequence Charts (HMSCs), an
MSC formalism describing potentially infinite sets of potentially unbounded
behaviours. To improve this negative situation for HMSCs, we introduce two
new notions: a new concept of race called trace-race and an extension of the
HMSC formalism with open coregions, i.e. coregions that can extend over more
than one BMSC. We present three arguments showing benefits of our notions
over the standard notions of race and HMSC. First, every trace-race-free
HMSC is also race-free. Second, every race-free HMSC can be equivalently
expressed as a trace-race-free HMSC with open coregions. Last, the
trace-race detection problem for HMSC with open coregions is decidable and
PSPACE-complete. Finally, the proposed extension of coregions allows to
represent in a visual fashion whether an arbitrary number of racing events
in the usual MSC formalism are concurrent or not.