skip to main content
research-article

The type discipline of behavioral separation

Published: 23 January 2013 Publication History

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.

Supplementary Material

JPG File (r2d2_talk1.jpg)
MP4 File (r2d2_talk1.mp4)

References

[1]
M. Abadi, C. Flanagan, and S. N. Freund. Types for safe locking: Static race detection for Java. ACM TOPLAS, 28(2):207--255, 2006.
[2]
A. Ahmed, M. Fluet, and G. Morrisett. L3: A Linear Language with Locations. Fundam. Inform., 77(4):397--449, 2007.
[3]
K. Bierhoff and J. Aldrich. Modular Typestate Checking of Aliased Objects. In OOPSLA 2007, pages 301--320, 2007.
[4]
S. L. Bloom and Z. Ésik. Free Shuffle Algebras in Language Varieties. Theoretical Computer Science, 163(1&2):55--98, 1996.
[5]
R. Bornat, C. Calcagno, P. W. O'Hearn, and M. Parkinson. Permission accounting in separation logic. In POPL 2005, pages 259--270, 2005.
[6]
C. Boyapati, R. Lee, and M. C. Rinard. Ownership types for safe programming: preventing data races and deadlocks. In OOPSLA 2002, pages 211--230. ACM, 2002.
[7]
C. Boyapati, B. Liskov, and L. Shrira. Ownership types for object encapsulation. In POPL 2003, 2003.
[8]
C. Boyapati and M. C. Rinard. A Parameterized Type System for Race-Free Java Programs. In OOPSLA 2001, pages 56--69, 2001.
[9]
J. Boyland. Checking Interference with Fractional Permissions. In SAS 2003, volume 2694 of LNCS, pages 55--72. Springer-Verlag, 2003.
[10]
L. Caires. Spatial-Behavioral Types for Concurrency and Resource Control in Distributed Systems. Theoretical Computer Science, 402(2--3):120--141, 2008.
[11]
L. Caires and L. Cardelli. A Spatial Logic for Concurrency (Part I). Information and Computation, 186(2):194--235, 2003.
[12]
L. Caires and F. Pfenning. Session Types as Intuitionistic Linear Propositions. In CONCUR'10, volume 6269 of LNCS, pages 222--236. Springer-Verlag, 2010.
[13]
L. Caires and J. C. Seco. The Type Discipline of Behavioral Separation. Technical report, TR-DI-FCT-UNL, 2012.
[14]
C. Calcagno, P. W. O'Hearn, and H. Yang. Local Action and Abstract Separation Logic. In LICS 2007, pages 366--378, 2007.
[15]
L. Cardelli and A. D. Gordon. Anytime, Anywhere. Modal Logics for Mobile Ambients. In POPL 2000, pages 365--377. ACM, 2000.
[16]
S. Chaki, S. Rajamani, and J. Rehof. Types as models: Model Checking Message-Passing Programs. In POPL 2002, pages 45--57, 2002.
[17]
T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis. Concurrent Abstract Predicates. In ECOOP 2010, volume 6183 of LNCS, pages 504--528. Springer-Verlag, 2010.
[18]
S. J. Gay, V. Thudichum Vasconcelos, A. Ravara, N. Gesbert, and A. Z. Caldeira. Modular Session Types for Distributed Object-oriented Programming. In POPL 2010, pages 299--312, 2010.
[19]
C. A. R. Hoare, B. Möller, G. Struth, and I. Wehrman. Concurrent Kleene Algebra. In CONCUR'09, volume 5710 of LNCS, pages 399--414. Springer-Verlag, 2009.
[20]
T. Hoare and P. W. O'Hearn. Separation Logic Semantics for Communicating Processes. EN Theo. Computer Science, 212:3--25, 2008.
[21]
K. Honda, V. T. Vasconcelos, and M. Kubo. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP 1998, volume 1381 of LNCS, pages 122--138. Springer, 1998.
[22]
K. Honda, N. Yoshida, and M. Carbone. Multiparty Asynchronous Session Types. In POPL 2008, pages 273--284. ACM, 2008.
[23]
A. Igarashi and N. Kobayashi. Resource Usage Analysis. In POPL 2002, pages 331--342, 2002.
[24]
A. Igarashi and N. Kobayashi. A Generic Type System for the Pi-Calculus. Theoretical Computer Science, 311(1--3):121--163, 2004.
[25]
J. B. Jensen and L. Birkedal. Fictional Separation Logic. In ESOP 2012, LNCS, pages 377--396. Springer-Verlag, 2012.
[26]
Cliff B. Jones. Splitting Atoms Safely. Theoretical Computer Science, 375(1--3):109--119, 2007.
[27]
R. Bocchino Jr., S. Heumann, N. Honarmand, S. Adve, V. Adve, A. Welc, and T. Shpeisman. Safe Nondeterminism in a Deterministic-by-default Parallel Language. In POPL 2011, pages 535--548, 2011.
[28]
N. R. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially Substructural Types. In ICFP'12, pages 41--54. ACM, 2012.
[29]
Militao, F. and Aldrich, J. and Caires, L. Aliasing control with view-based typestate. In FTFJP '10, pages 7:1--7:7. ACM, 2010.
[30]
K. Naden, R. Bocchino, J. Aldrich, and K. Bierhoff. A Type System for Borrowing Permissions. In POPL 2012, pages 557--570, 2012.
[31]
A. Nanevski, J. G. Morrisett, and L. Birkedal. Hoare Type Theory, Polymorphism and Separation. J. Fun. P., 18(5--6):865--911, 2008.
[32]
P. W. O'Hearn. On Bunched Typing. J. Fun. P., 13(4):747--796, 2003.
[33]
P. W. O'Hearn. Resources, Concurrency, and Local Reasoning. Theor. Comput. Sci., 375(1--3):271--307, 2007.
[34]
B. Pierce. Types and Programming Languages. MIT Press, 2002.
[35]
François Pottier. Hiding local state in direct style: A higher-order anti-frame rule. In LICS'08, pages 331--340, 2008.
[36]
J. C. Reynolds. Syntactic Control of Interference. In POPL 78, pages 39--46, 1978.
[37]
J. C. Reynolds. Syntactic Control of Interference, Part 2. In ICALP 89, volume 372 of LNCS, pages 704--722. Springer, 1989.
[38]
J. C. Reynolds. Design of the programming language FORSYTHE, pages 173--233. Birkhauser Boston Inc., Cambridge, MA, USA, 1997.
[39]
J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2012, 2002.
[40]
J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested Hoare Triples and Frame Rules for Higher-order Store. Logical Methods in Computer Science, 7(3), 2011.
[41]
J. Villard, E. Lozes, and C. Calcagno. Proving copyless message passing. In APLAS 2009, volume 5904 of LNCS, pages 194--209. Springer-Verlag, 2009.

Cited By

View all
  • (2021)Papaya: Global Typestate Analysis of Aliased ObjectsProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming10.1145/3479394.3479414(1-13)Online publication date: 6-Sep-2021
  • (2021)Behavioural separation with parallel usagesProceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3464971.3468424(51-58)Online publication date: 13-Jul-2021
  • (2020)Behavioural Types for Memory and Method Safety in a Core Object-Oriented LanguageProgramming Languages and Systems10.1007/978-3-030-64437-6_6(105-124)Online publication date: 24-Nov-2020
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. behavioral types
  2. concurrency
  3. higher order programming
  4. interference
  5. separation

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)7
  • Downloads (Last 6 weeks)1
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2021)Papaya: Global Typestate Analysis of Aliased ObjectsProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming10.1145/3479394.3479414(1-13)Online publication date: 6-Sep-2021
  • (2021)Behavioural separation with parallel usagesProceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3464971.3468424(51-58)Online publication date: 13-Jul-2021
  • (2020)Behavioural Types for Memory and Method Safety in a Core Object-Oriented LanguageProgramming Languages and Systems10.1007/978-3-030-64437-6_6(105-124)Online publication date: 24-Nov-2020
  • (2018)Automated Modular Verification for Relaxed Communication ProtocolsProgramming Languages and Systems10.1007/978-3-030-02768-1_16(284-305)Online publication date: 22-Oct-2018
  • (2017)Verifying Concurrent Programs Using Contracts2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2017.25(196-206)Online publication date: Mar-2017
  • (2016)LaCasa: lightweight affinity and object capabilities in ScalaACM SIGPLAN Notices10.1145/3022671.298404251:10(272-291)Online publication date: 19-Oct-2016
  • (2023)Safe Session-Based Concurrency with Shared Linear StateProgramming Languages and Systems10.1007/978-3-031-30044-8_16(421-450)Online publication date: 22-Apr-2023
  • (2021)Propositions-as-types and shared stateProceedings of the ACM on Programming Languages10.1145/34735845:ICFP(1-30)Online publication date: 19-Aug-2021
  • (2016)LaCasa: lightweight affinity and object capabilities in ScalaACM SIGPLAN Notices10.1145/3022671.298404251:10(272-291)Online publication date: 19-Oct-2016
  • (2016)LaCasa: lightweight affinity and object capabilities in ScalaProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2983990.2984042(272-291)Online publication date: 19-Oct-2016
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media