Behavioural Separation with Parallel Usages for a Core Object-Oriented Language
Authors
Golovanov, Iaroslav ; Jakobsen, Mathias Steen ; Kettunen, Mikkel Klinke
Term
4. term
Education
Publication year
2020
Submitted on
2020-06-15
Abstract
This thesis extends the object-oriented language Mungo with behavioral separation through a new parallel usage construct that allows an object to be split into two local protocols and later merged. The aim is to relax the linear typing discipline that forbids aliasing and to concisely express unrelated operations, avoiding exponential protocol specifications. Drawing on separation logic and behavioral separation, parallel usages enable local reasoning about heap-separated parts and limited aliasing in method calls. We define the language’s syntax and types, introduce both big-step and small-step operational semantics, and prove their equivalence for terminating programs. We present a type system and show that Mungo’s prior guarantees are preserved: protocol fidelity, safety, and progress, with the latter preventing null dereferencing at runtime. We also discuss alternative typestate approaches in Mungo, Plaid, and Fugue. Finally, we provide an implementation of Mungo with parallel usages and example programs that demonstrate how real-world protocols can be expressed and enforced.
Dette speciale udvider det objektorienterede sprog Mungo med adfærdsmæssig separation via en ny parallel-usage-konstruktion, der gør det muligt at splitte et objekt i to lokale protokoller og senere samle dem igen. Målet er at mindske den lineære typningsdisciplin, hvor aliaser er forbudt, og samtidig beskrive uafhængige operationer mere kortfattet for at undgå eksplosiv vækst i protokoller. Arbejdet er inspireret af separation logic og behavioural separation, og parallelle usages bruges til at ræsonnere lokalt om heap-adskilte dele og om begrænset aliasing i metodekald. Vi definerer sprogsyntaks og -typer, introducerer både big-step- og small-step-semantik og viser ækvivalens for terminerende programmer. Vi præsenterer et typesystem og beviser, at tidligere garantier for Mungo bevares: protokolfidelitet, sikkerhed (safety) og fremdrift (progress), hvor sidstnævnte udelukker null-dereferering ved kørsel. Derudover diskuterer vi typestate-tilgange i Mungo, Plaid og Fugue. Endelig giver vi en implementering af Mungo med parallelle usages samt eksempelprogrammer, der viser, hvordan konstruktionen udtrykker virkelige protokoller og hjælper med at sikre, at de følges.
[This apstract has been generated with the help of AI directly from the project full text]