Luís Caires
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.
Supplemental Material
- M. Abadi, C. Flanagan, and S. N. Freund. Types for safe locking: Static race detection for Java. ACM TOPLAS, 28(2):207--255, 2006. Google Scholar
Digital Library
- A. Ahmed, M. Fluet, and G. Morrisett. L3: A Linear Language with Locations. Fundam. Inform., 77(4):397--449, 2007. Google ScholarDigital Library
- K. Bierhoff and J. Aldrich. Modular Typestate Checking of Aliased Objects. In OOPSLA 2007, pages 301--320, 2007. Google ScholarDigital Library
- S. L. Bloom and Z. Ésik. Free Shuffle Algebras in Language Varieties. Theoretical Computer Science, 163(1&2):55--98, 1996. Google ScholarDigital Library
- R. Bornat, C. Calcagno, P. W. O'Hearn, and M. Parkinson. Permission accounting in separation logic. In POPL 2005, pages 259--270, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- C. Boyapati, B. Liskov, and L. Shrira. Ownership types for object encapsulation. In POPL 2003, 2003. Google ScholarDigital Library
- C. Boyapati and M. C. Rinard. A Parameterized Type System for Race-Free Java Programs. In OOPSLA 2001, pages 56--69, 2001. Google ScholarDigital Library
- J. Boyland. Checking Interference with Fractional Permissions. In SAS 2003, volume 2694 of LNCS, pages 55--72. Springer-Verlag, 2003. Google ScholarDigital Library
- L. Caires. Spatial-Behavioral Types for Concurrency and Resource Control in Distributed Systems. Theoretical Computer Science, 402(2--3):120--141, 2008. Google ScholarDigital Library
- L. Caires and L. Cardelli. A Spatial Logic for Concurrency (Part I). Information and Computation, 186(2):194--235, 2003. Google ScholarDigital Library
- L. Caires and F. Pfenning. Session Types as Intuitionistic Linear Propositions. In CONCUR'10, volume 6269 of LNCS, pages 222--236. Springer-Verlag, 2010. Google ScholarDigital Library
- L. Caires and J. C. Seco. The Type Discipline of Behavioral Separation. Technical report, TR-DI-FCT-UNL, 2012.Google Scholar
- C. Calcagno, P. W. O'Hearn, and H. Yang. Local Action and Abstract Separation Logic. In LICS 2007, pages 366--378, 2007. Google ScholarDigital Library
- L. Cardelli and A. D. Gordon. Anytime, Anywhere. Modal Logics for Mobile Ambients. In POPL 2000, pages 365--377. ACM, 2000. Google ScholarDigital Library
- S. Chaki, S. Rajamani, and J. Rehof. Types as models: Model Checking Message-Passing Programs. In POPL 2002, pages 45--57, 2002. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- T. Hoare and P. W. O'Hearn. Separation Logic Semantics for Communicating Processes. EN Theo. Computer Science, 212:3--25, 2008. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- K. Honda, N. Yoshida, and M. Carbone. Multiparty Asynchronous Session Types. In POPL 2008, pages 273--284. ACM, 2008. Google ScholarDigital Library
- A. Igarashi and N. Kobayashi. Resource Usage Analysis. In POPL 2002, pages 331--342, 2002. Google ScholarDigital Library
- A. Igarashi and N. Kobayashi. A Generic Type System for the Pi-Calculus. Theoretical Computer Science, 311(1--3):121--163, 2004. Google ScholarDigital Library
- J. B. Jensen and L. Birkedal. Fictional Separation Logic. In ESOP 2012, LNCS, pages 377--396. Springer-Verlag, 2012. Google ScholarDigital Library
- Cliff B. Jones. Splitting Atoms Safely. Theoretical Computer Science, 375(1--3):109--119, 2007. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- N. R. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially Substructural Types. In ICFP'12, pages 41--54. ACM, 2012. Google ScholarDigital Library
- Militao, F. and Aldrich, J. and Caires, L. Aliasing control with view-based typestate. In FTFJP '10, pages 7:1--7:7. ACM, 2010. Google ScholarDigital Library
- K. Naden, R. Bocchino, J. Aldrich, and K. Bierhoff. A Type System for Borrowing Permissions. In POPL 2012, pages 557--570, 2012. Google ScholarDigital Library
- A. Nanevski, J. G. Morrisett, and L. Birkedal. Hoare Type Theory, Polymorphism and Separation. J. Fun. P., 18(5--6):865--911, 2008. Google ScholarDigital Library
- P. W. O'Hearn. On Bunched Typing. J. Fun. P., 13(4):747--796, 2003. Google ScholarDigital Library
- P. W. O'Hearn. Resources, Concurrency, and Local Reasoning. Theor. Comput. Sci., 375(1--3):271--307, 2007. Google ScholarDigital Library
- B. Pierce. Types and Programming Languages. MIT Press, 2002. Google ScholarDigital Library
- François Pottier. Hiding local state in direct style: A higher-order anti-frame rule. In LICS'08, pages 331--340, 2008. Google ScholarDigital Library
- J. C. Reynolds. Syntactic Control of Interference. In POPL 78, pages 39--46, 1978. Google ScholarDigital Library
- J. C. Reynolds. Syntactic Control of Interference, Part 2. In ICALP 89, volume 372 of LNCS, pages 704--722. Springer, 1989. Google ScholarDigital Library
- J. C. Reynolds. Design of the programming language FORSYTHE, pages 173--233. Birkhauser Boston Inc., Cambridge, MA, USA, 1997. Google ScholarDigital Library
- J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2012, 2002. Google ScholarDigital Library
- 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.Google Scholar
- J. Villard, E. Lozes, and C. Calcagno. Proving copyless message passing. In APLAS 2009, volume 5904 of LNCS, pages 194--209. Springer-Verlag, 2009. Google ScholarDigital Library
Index Terms
- The type discipline of behavioral separation
Recommendations
The type discipline of behavioral separation
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe 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-...
A behavioral type system and its application in Ptolemy II
Abstract.Interface automata [deH01] have been introduced as an interface theory [deH01a] capable of functioning as a behavioral type system. Behavioral type systems describe dynamic properties of components and their compositions. Like traditional (data) ...
Concurrent typed intermediate language
SAC '13: Proceedings of the 28th Annual ACM Symposium on Applied ComputingTyped assembly languages have been designed to ensure safety on low-level code, avoiding the dynamic loading of erroneous code, generated by unreliable compilers, thus compromising the correct behavior of virtual machines and processors. Among the most ...
Comments