Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Session Abstract Machine (Extended Version)

Luís Caires, Bernardo Toninho

TL;DR

The paper introduces the Session Abstract Machine (SAM), a deterministic, sequential execution model for session-typed processes grounded in classical linear logic ($\mathsf{CLL}$). It couples a write-biased, queue-based channel semantics with an intermediate buffered language ($\mathsf{CLLB}$) to achieve correct, compilable execution and to connect logical proofs with operational behavior. The authors prove preservation, progress, and a tight operational correspondence between $\mathsf{CLL}$, $\mathsf{CLLB}$, and SAM, and extend the core machine to handle exponentials and a modular concurrent interpretation of cut and mix. An implemented SAM-based artifact demonstrates practical feasibility, and the work positions the SAM as a principled foundation for multi-paradigm session-based programming languages with static safety guarantees. The results advance understanding of how fine-grained session types and linear resources can be realized in concrete, concurrent runtimes.

Abstract

We build on a fine-grained analysis of session-based interaction as provided by the linear logic typing disciplines to introduce the SAM, an abstract machine for mechanically executing session-typed processes. A remarkable feature of the SAM's design is its ability to naturally segregate and coordinate sequential with concurrent session behaviours. In particular, implicitly sequential parts of session programs may be efficiently executed by deterministic sequential application of SAM transitions, amenable to compilation, and without concurrent synchronisation mechanisms. We provide an intuitive discussion of the SAM structure and its underlying design, and state and prove its correctness for executing programs in a session calculus corresponding to full classical linear logic CLL. We also discuss extensions and applications of the SAM to the execution of linear and session-based programming languages.

The Session Abstract Machine (Extended Version)

TL;DR

The paper introduces the Session Abstract Machine (SAM), a deterministic, sequential execution model for session-typed processes grounded in classical linear logic (). It couples a write-biased, queue-based channel semantics with an intermediate buffered language () to achieve correct, compilable execution and to connect logical proofs with operational behavior. The authors prove preservation, progress, and a tight operational correspondence between , , and SAM, and extend the core machine to handle exponentials and a modular concurrent interpretation of cut and mix. An implemented SAM-based artifact demonstrates practical feasibility, and the work positions the SAM as a principled foundation for multi-paradigm session-based programming languages with static safety guarantees. The results advance understanding of how fine-grained session types and linear resources can be realized in concrete, concurrent runtimes.

Abstract

We build on a fine-grained analysis of session-based interaction as provided by the linear logic typing disciplines to introduce the SAM, an abstract machine for mechanically executing session-typed processes. A remarkable feature of the SAM's design is its ability to naturally segregate and coordinate sequential with concurrent session behaviours. In particular, implicitly sequential parts of session programs may be efficiently executed by deterministic sequential application of SAM transitions, amenable to compilation, and without concurrent synchronisation mechanisms. We provide an intuitive discussion of the SAM structure and its underlying design, and state and prove its correctness for executing programs in a session calculus corresponding to full classical linear logic CLL. We also discuss extensions and applications of the SAM to the execution of linear and session-based programming languages.
Paper Structure (19 sections, 14 theorems, 45 equations, 14 figures)

This paper contains 19 sections, 14 theorems, 45 equations, 14 figures.

Table of Contents

  1. Introduction
  2. Background on $\mathsf{CLL}$, the core language and type system
  3. A Core Session Abstract Machine
  4. On the Write-Bias of the SAM
  5. Illustrating Forwarding
  6. $\mathsf{CLLB}$: A Buffered Formulation of $\mathsf{CLL}$
  7. Preservation and Progress for $\mathsf{CLLB}$
  8. Correspondence between $\mathsf{CLL}$ and $\mathsf{CLLB}$
  9. Correctness of the core SAM
  10. The SAM for full $\mathsf{CLL}$
  11. Concurrent Semantics of Cut and Mix
  12. Concluding Remarks and Related Work
  13. Acknowledgments.
  14. Appendix - Supplementary Material
  15. Proofs of Section \ref{['sec:safetyCLLB']}: Preservation and Progress for $\mathsf{CLLB}$
  16. ...and 4 more sections

Key Result

theorem 1

Let $P \vdash \Delta; \Gamma$. (1) If $P \equiv Q$, then $Q \vdash \Delta; \Gamma$. (2) If $P \to Q$, then $Q \vdash \Delta; \Gamma$.

Figures (14)

  • Figure 1: Typing Rules of $\mathsf{CLL}$.
  • Figure 2: Structural congruence $P \equiv Q$.
  • Figure 3: Reduction $P \to Q$.
  • Figure 4: core SAM Components
  • Figure 5: The core SAM Transition Rules
  • ...and 9 more figures

Theorems & Definitions (51)

  • definition 1: Types
  • definition 2: Processes
  • definition 3: $P \equiv Q$
  • definition 4: Reduction $\to$
  • theorem 1: Type Preservation
  • theorem 2: Progress
  • definition 5: Setting polarities
  • definition 6: Embedding
  • definition 7: Typing of Queue Values
  • proof
  • ...and 41 more