Stateful Behavioral Types for Active Objects

DOI10.1007/978-3-319-98938-9_13MaRDI QIDQ6104495zbMATH OpenOpenAlexFDO

Authors

Publication date 28 June 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1802.08492

zbMATH Keywords

asynchronous method callsbehavioral typesglobal typeheap memoryprotocol adherence

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: It is notoriously hard to correctly implement a multiparty protocol which involves asynchronous/concurrent interactions and the constraints on states of multiple participants. To assist developers in implementing such protocols, we propose a novel specification language to specify interactions within multiple object-oriented actors and the side-effects on heap memory of those actors; a behavioral-type-based analysis is presented for type checking. Our specification language formalizes a protocol as a global type, which describes the procedure of asynchronous method calls, the usage of futures, and the heap side-effects with a first-order logic. To characterize runs of instances of types, we give a model-theoretic semantics for types and translate them into logical constraints over traces. We prove protocol adherence: If a program is well-typed w.r.t. a protocol, then every trace of the program adheres to the protocol, i.e., every trace is a model for the formula of its type.

Recommendations

• Modular session types for objects
• Modular session types for distributed object-oriented programming
• Multiparty session actors
• Multiparty asynchronous session types
• CONCUR 2004 - Concurrency Theory

Cites work

• A sound and complete reasoning system for asynchronous communication with shared futures
• A theory of design-by-contract for distributed multiparty interactions
• An axiomatic basis for computer programming
• Certifying data in multiparty session types
• Characteristic formulae for session types
• Dynamic frames in Java dynamic logic
• First-order dynamic logic
• scientific article; zbMATH DE number 6851955 (Why is no real title available?)
• scientific article; zbMATH DE number 3248820 (Why is no real title available?)
• Key-ABS: a deductive verification tool for the concurrent modelling language ABS
• May-happen-in-parallel analysis for actor-based concurrency
• Modular session types for objects
• Multiparty Asynchronous Session Types
• Objects and session types
• Session types as intuitionistic linear propositions
• Symbolic execution and program testing

Cited in

(8)

• Behavioural types for memory and method safety in a core object-oriented language
• scientific article; zbMATH DE number 6721685 (Why is no real title available?)
• Global protocol implementations via attribute-based communication
• State inference for dynamically changing interfaces
• scientific article; zbMATH DE number 1860620 (Why is no real title available?)
• Strong types for coordinating active objects
• Featherweight Scribble
• Asynchronous Cooperative Contracts for Cooperative Scheduling

This page was built for publication: Stateful Behavioral Types for Active Objects

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6104495)