Skip to Main content Skip to Navigation
Conference papers

Exposing Latent Mutual Exclusion by Work Automata

Abstract : A concurrent application consists of a set of concurrently executing interacting processes. Although earlier we proposed work automata to specify both computation and interaction of such a set of executing processes, a detailed formal semantics for them was left implicit. In this paper, we provide a formal semantics for work automata, based on which we introduce equivalences such as weak simulation and weak language inclusion. Subsequently, we define operations on work automata that simplify them while preserving these equivalences. Where applicable, these operations simplify a work automaton by merging its different states into a state with a ‘more inclusive’ state-invariant. The resulting state-invariant defines a region in a multidimensional real vector space that potentially contains holes, which in turn expose mutual exclusion among processes. Such exposed dependencies provide additional insight in the behavior of an application, which can enhance scheduling. Our operations, therefore, potentially expose implicit dependencies among processes that otherwise may not be evident to exploit.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, April 6, 2018 - 3:08:11 PM
Last modification on : Friday, April 6, 2018 - 3:08:57 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Kasper Dokter, Farhad Arbab. Exposing Latent Mutual Exclusion by Work Automata. 2nd International Conference on Topics in Theoretical Computer Science (TTCS), Sep 2017, Tehran, Iran. pp.59-73, ⟨10.1007/978-3-319-68953-1_6⟩. ⟨hal-01760644⟩



Record views


Files downloads