A Petri Net Based Modeling of Active Objects and Futures

Abstract : We give two different notions of deadlock for systems based on active objects and futures. One is based on blocked objects and conforms with the classical definition of deadlock by Coffman, Jr. et al. The other one is an extended notion of deadlock based on blocked processes which is more general than the classical one. We introduce a technique to prove deadlock freedom of systems of active objects. To check deadlock freedom an abstract version of the program is translated into Petri nets. Extended deadlocks, and then also classical deadlock, can be detected via checking reachability of a distinct marking. Absence of deadlocks in the Petri net constitutes deadlock freedom of the concrete system.
Document type :
Journal articles
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01919136
Contributor : Mario Bravetti <>
Submitted on : Monday, November 12, 2018 - 11:25:03 AM
Last modification on : Wednesday, November 14, 2018 - 3:09:53 PM
Long-term archiving on : Wednesday, February 13, 2019 - 1:18:49 PM

File

fundainfo.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Frank de Boer, Mario Bravetti, Matias Lee, Gianluigi Zavattaro. A Petri Net Based Modeling of Active Objects and Futures. Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2018, 159 (3), pp.197-256. ⟨10.3233/FI-2018-1663⟩. ⟨hal-01919136⟩

Share

Metrics

Record views

133

Files downloads

106