Thumbnail
Access Restriction
Subscribed

Author Caires, Luís ♦ Seco, João C.
Source ACM Digital Library
Content type Audio ♦ Text
Publisher Association for Computing Machinery (ACM)
File Format PDF ♦ MP4
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
Subject Keyword Higher order programming ♦ Behavioral types ♦ Separation ♦ Concurrency ♦ Interference
Abstract We introduce the concept of behavioral separation as a general principle for disciplining interference in higher-order imperative concurrent programs, and present a type-based approach that systematically develops the concept in the context of an ML-like language extended with concurrency and synchronization primitives. Behavioral separation builds on notions originally introduced for behavioral type systems and separation logics, but shifts the focus from the separation of static program state properties towards the separation of dynamic usage behaviors of runtime values. Behavioral separation types specify how values may be safely used by client code, and can enforce fine-grained interference control disciplines while preserving compositionality, information hiding, and flexibility. We illustrate how our type system, even if based on a small set of general primitives, is already able to tackle fairly challenging program idioms, involving aliasing at various types, concurrency with first-class threads, manipulation of linked data structures, behavioral borrowing, and invariant-based separation.
Description Affiliation: Universidade Nova de Lisboa, Lisboa, Portugal (Caires, Luís; Seco, João C.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1983-05-01
Publisher Place New York
Journal ACM SIGPLAN Notices (SIGP)
Volume Number 48
Issue Number 1
Page Count 12
Starting Page 275
Ending Page 286


Open content in new tab

   Open content in new tab
Source: ACM Digital Library