Behavioural separation with parallel usages

Iaroslav Golovanov, Hans Hüttel, Mathias Jakobsen, Mikkel Kettunen

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

1 Citationer (Scopus)

Abstract

Mungo is an object-oriented language that uses typestates with a behavioural type system to ensure the absence of null-dereferencing. Typestates are usages that specify the admissible sequences of method calls on objects. Previous type systems for Mungo have all had a linearity constraint on objects. We present an extension of these systems, where usage specifications can now include a parallel construct that lets us describe separate local behaviour. A parallel usage describes a separation of the heap, and this allows us to reason about aliasing and to express arbitrary interleaving of local protocols. This also solves the state-space explosion problem for usages. Our extension retains the safety properties of previous type systems for Mungo.

OriginalsprogEngelsk
TitelFTfJP 2021 - Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, co-located with ECOOP/ISSTA 2021
RedaktørerDavid R. Cok
Antal sider8
ForlagAssociation for Computing Machinery
Publikationsdato13 jul. 2021
Sider51-58
ISBN (Elektronisk)978-1-4503-8543-5
DOI
StatusUdgivet - 13 jul. 2021
Begivenhed23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021 - Virtual, Online, Danmark
Varighed: 13 jul. 202113 jul. 2021

Konference

Konference23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021
Land/OmrådeDanmark
ByVirtual, Online
Periode13/07/202113/07/2021
SponsorACM SIGPLAN

Bibliografisk note

Publisher Copyright:
© 2021 ACM.

Fingeraftryk

Dyk ned i forskningsemnerne om 'Behavioural separation with parallel usages'. Sammen danner de et unikt fingeraftryk.

Citationsformater