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

https://hal.inria.fr/hal-01760644
Contributor : Hal Ifip <>
Submitted on : Friday, April 6, 2018 - 3:08:11 PM
Last modification on : Friday, April 6, 2018 - 3:08:57 PM

File

440117_1_En_6_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

103

Files downloads

64