More Web Proxy on the site http://driver.im/

research-article

Open access

Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types

Authors:

Colin S. Gordon,

Michael D. Ernst,

Matthew J. ParkinsonAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 39, Issue 3

Article No.: 11, Pages 1 - 54

https://doi.org/10.1145/3064850

Published: 10 May 2017 Publication History

Abstract

Verifying invariants of fine-grained concurrent data structures is challenging, because interference from other threads may occur at any time. We propose a new way of proving invariants of fine-grained concurrent data structures: applying rely-guarantee reasoning to references in the concurrent setting. Rely-guarantee applied to references can verify bounds on thread interference without requiring a whole program to be verified.

This article provides three new results. First, it provides a new approach to preserving invariants and restricting usage of concurrent data structures. Our approach targets a space between simple type systems and modern concurrent program logics, offering an intermediate point between unverified code and full verification. Furthermore, it avoids sealing concurrent data structure implementations and can interact safely with unverified imperative code. Second, we demonstrate the approach’s broad applicability through a series of case studies, using two implementations: an axiomatic Coq domain-specific language and a library for Liquid Haskell. Third, these two implementations allow us to compare and contrast verifications by interactive proof (Coq) and a weaker form that can be expressed using automatically-discharged dependent refinement types (Liquid Haskell).

References

[1]

Pieter Agten, Bart Jacobs, and Frank Piessens. 2015. Sound modular verification of c code executing in an unverified context. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’15).

Digital Library

[2]

Richard J. Anderson and Heather Woll. 1991. Wait-free parallel algorithms for the union-find problem. In Proceedings of the Symposium on Theory of Computing (STOC’91).

Digital Library

[3]

Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development; Coq’Art: The Calculus of Inductive Constructions. Springer Verlag.

Digital Library

[4]

John Boyland. 2003. Checking interference with fractional permissions. In Proceedings of the Static Analysis Symposium (SAS’03).

Digital Library

[5]

Stephen Brookes. 2004. A semantics for concurrent separation logic. In Proceedings of the International Conference on Concurrency Theory (CONCUR’04).

[6]

Venanzio Capretta. 2004. A Polymorphic Representation of Induction-Recursion. Retrieved September 12, 2012 from http://www.cs.ru.nl/&sim;enanzio/publications/induction_recursion.pdf.

[7]

Adam Chlipala. 2011. Mostly-automated verification of low-level programs in computational separation logic. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’11).

Digital Library

[8]

Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2009. Effective interactive proofs for higher-order imperative programs. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’09).

Digital Library

[9]

Vasek Chvatal. 1983. Linear Programming. Macmillan.

[10]

Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A practical system for verifying concurrent C. In Proceedings of the International Conference on Theorem Proving in Higher Order Logics (TPHOL’09).

Digital Library

[11]

Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies. 2010. Local verification of global invariants in concurrent programs. In Proceedings of the International Conference on Computer-Aided Verification (CAV’10).

Digital Library

[12]

Thierry Coquand and Gerard Huet. 1988. The calculus of constructions. Inform. Comput. 76, 2 (1988), 95--120.

Digital Library

[13]

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, Third Edition (3rd ed.). The MIT Press.

Digital Library

[14]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A logic for time and data abstraction. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP’14).

Digital Library

[15]

Edsger W. Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8 (Aug. 1975), 453--457.

Digital Library

[16]

Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang. 2013. Views: Compositional reasoning for concurrent programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13).

Digital Library

[17]

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, and Viktor Vafeiadis. 2010. Concurrent abstract predicates. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP’10).

Digital Library

[18]

Mike Dodds, Xinyu Feng, Matthew Parkinson, and Viktor Vafeiadis. 2009. Deny-guarantee reasoning. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’09).

Digital Library

[19]

Peter Dybjer. 2000. A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symbol. Logic 65, 02 (2000), 525--549.

[20]

Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, and Serdar Tasiran. 2010. Simplifying linearizability proofs with reduction and abstraction. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS).

Digital Library

[21]

Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. 2009. A calculus of atomic actions. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09).

Digital Library

[22]

Xinyu Feng. 2009. Local rely-guarantee reasoning. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09).

Digital Library

[23]

Cormac Flanagan and Martín Abadi. 1999. Types for safe locking. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’99).

Digital Library

[24]

Cormac Flanagan and Stephen N. Freund. 2000. Type-based race detection for java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’00).

Digital Library

[25]

Fredrik Nordvall Forsberg and Anton Setzer. 2010. Inductive-inductive definitions. In Proceedings of the International Workshop on Computer Science Logic. Springer, 454--468.

Digital Library

[26]

Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’91).

Digital Library

[27]

Colin S. Gordon. 2014. Verifying Concurrent Programs by Controlling Alias Interference. Ph.D. Thesis. University of Washington.

[28]

Colin S. Gordon, Michael D. Ernst, and Dan Grossman. 2013. Rely-guarantee references for refinement types over aliased mutable data. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’13).

Digital Library

[29]

Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. 2012. Uniqueness and reference immutability for safe parallelism. In Proceedings of the ACM International Object Oriented Programming Systems Languages and Applications (OOPSLA’12).

Digital Library

[30]

Timothy L Harris. 2001. A pragmatic implementation of non-blocking linked-lists. In Proceedings of the International Symposium on Distributed Computing (DISC’01).

Digital Library

[31]

Steve Heller, Maurice Herlihy, Victor Luchangco, Mark Moir, William N. Scherer, and Nir Shavit. 2006. A lazy concurrent list-based set algorithm. In Proceedings of the International Conference on Principles of Distributed Systems (OPODIS’05).

Digital Library

[32]

Danny Hendler, Nir Shavit, and Lena Yerushalmi. 2004. A scalable lock-free stack algorithm. In Proceedings of the ACM Symposium on Parallelism in Algorithms and Architectures (SPAA’04).

Digital Library

[33]

Maurice Herlihy. 1991. Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13, 1 (Jan. 1991), 124--149.

Digital Library

[34]

Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA.

Digital Library

[35]

C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576--580.

Digital Library

[36]

Wei Huang, Ana Milanova, Werner Dietl, and Michael D Ernst. 2012. ReIm 8 ReImInfer: Checking and inference of reference immutability and method purity. In Proceedings of the ACM International Object Oriented Programming Systems Languages and Applications (OOPSLA’12).

Digital Library

[37]

Bart Jacobs and Frank Piessens. 2011. Expressive modular fine-grained concurrency specification. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11).

Digital Library

[38]

Jonas Braband Jensen and Lars Birkedal. 2012. Fictional separation logic. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’12).

Digital Library

[39]

Ranjit Jhala. 2015. LiquidHaskell: Refinement Types for Haskell. Retrieved from http://www. degoesconsulting.com/lambdaconf-2015/#talk-6f64790e6c.

[40]

Ranjit Jhala. 2016. Programming with Refinement Types. Retrieved from http://www.thestrangeloop.com/2015/programming-with-refinement-types.html.

[41]

Ranjit Jhala, Rupak Majumdar, and Andrey Rybalchenko. 2011. HMC: Verifying functional programs with abstract interpreters. In Proceedings of the International Conference on Computer-Aided Verification (CAV’11).

Digital Library

[42]

C. B. Jones. 1983. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5, 4 (Oct. 1983), 596--619.

Digital Library

[43]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’15).

Digital Library

[44]

Ming Kawaguchi, Patrick Rondon, Alexander Bakst, and Ranjit Jhala. 2012. Deterministic parallelism with liquid effects. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’12).

Digital Library

[45]

Ming Kawaguchi, Patrick Rondon, and Ranjit Jhala. 2009. Type-based data structure verification. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’09).

Digital Library

[46]

Ming Kawaguchi, Patrick M. Rondon, and Ranjit Jhala. 2010. Dsolve: Safety verification via liquid types. In Proceedings of the International Conference on Computer-Aided Verification (CAV’10).

Digital Library

[47]

Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. 2015. Asynchronous liquid separation types. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP’15).

[48]

Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective auxiliary state for coarse-grained concurrency. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13).

Digital Library

[49]

Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’13).

Digital Library

[50]

Barbara H. Liskov and Jeannette M. Wing. 1994. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16, 6 (Nov. 1994), 1811--1841.

Digital Library

[51]

Anil Madhavapeddy, Richard Mortier, Charalampos Rotsos, David Scott, Balraj Singh, Thomas Gazagnaire, Steven Smith, Steven Hand, and Jon Crowcroft. 2013. Unikernels: Library operating systems for the cloud. In Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’13).

Digital Library

[52]

Maged M. Michael. 2004. Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst. 15, 6 (2004), 491--504.

Digital Library

[53]

Maged M. Michael and Michael L. Scott. 1996. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proceedings of the Symposium on Principles of Distributed Computing (PODC’96).

Digital Library

[54]

Filipe Militão, Jonathan Aldrich, and Luís Caires. 2014. Rely-guarantee protocols. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP’14).

Digital Library

[55]

Filipe Militão, Jonathan Aldrich, and Luís Caires. 2016. Composing interfering abstract protocols. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP’16).

[56]

Aleksandar Nanevski, Paul Govereau, and Greg Morrisett. 2009. Towards type-theoretic semantics for transactional concurrency. In Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI’09).

Digital Library

[57]

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán André s Delbianco. 2014. Communicating state transition systems for fine-grained concurrent resources. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’14).

Digital Library

[58]

Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. 2008. Ynot: Dependent types for imperative programs. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’08).

Digital Library

[59]

Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. 2010. Structuring the verification of heap-manipulating programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10).

Digital Library

[60]

Peter O’Hearn, John Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In Proceedings of the International Workshop on Computer Science Logic (CSL’01).

Digital Library

[61]

Peter W. O’Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, and Greta Yorsh. 2010. Verifying linearizability with hindsight. In Proceedings of the Symposium on Principles of Distributed Computing (PODC’10).

Digital Library

[62]

Susan Owicki and David Gries. 1976. An axiomatic proof technique for parallel programs I. Acta Inform. Issue 6 (1976), 319--340.

Digital Library

[63]

Alexandre Pilkiewicz and François Pottier. 2011. The essence of monotonic state. In Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI’11).

Digital Library

[64]

François Pottier. 2008. Hiding local state in direct style: A higher-order anti-frame rule. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS’08).

Digital Library

[65]

Azalea Raad, Jules Villard, and Philippa Gardner. 2015. CoLoSL: Concurrent local subjective logic. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’15).

[66]

John C. Reynolds. 1988. Preliminary Design of the Programming Language Forsythe. Technical Report CMU-CS-88-159. Carnegie Mellon University.

[67]

Patrick Rondon. 2012. Liquid Types. Ph.D. Dissertation. University of California, San Diego.

Digital Library

[68]

Patrick Rondon, Alexander Bakst, Ming Kawaguchi, and Ranjit Jhala. 2012. CSolve: Verifying C with liquid types. In Proceedings of the International Conference on Computer-Aided Verification (CAV’12).

Digital Library

[69]

Patrick M. Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’08).

Digital Library

[70]

Patrick M. Rondon, Ming Kawaguchi, and Ranjit Jhala. 2010. Low-level liquid types. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10).

Digital Library

[71]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015a. Mechanized verification of fine-grained concurrent programs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’15).

Digital Library

[72]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015b. Specifying and verifying concurrent algorithms with histories and subjectivity. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’15).

Digital Library

[73]

Jan Smans, Dries Vanoverberghe, Dominique Devriese, Bart Jacobs, and Frank Piessens. 2014. Shared Boxes: Rely-Guarantee Reasoning in VeriFast. Technical Report CW622. KU Leuven.

[74]

Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’14).

Digital Library

[75]

Kasper Svendsen, Lars Birkedal, and Matthew Parkinson. 2013. Modular reasoning about separation of concurrent data structures. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’13).

Digital Library

[76]

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016. Dependent types and multi-monadic effects in F&star;. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’16).

Digital Library

[77]

Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’13).

Digital Library

[78]

R. Kent Treiber. 1986. Systems programming: Coping with parallelism. Technical Report. IBM Thomas J. Watson Research Center.

[79]

Matthew S. Tschantz and Michael D. Ernst. 2005. Javari: Adding reference immutability to java. In Proceedings of the ACM International Object Oriented Programming Systems Languages and Applications (OOPSLA’05).

Digital Library

[80]

Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’13).

Digital Library

[81]

Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro. 2006. Proving correctness of highly-concurrent linearisable objects. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’06).

Digital Library

[82]

Viktor Vafeiadis and Matthew Parkinson. 2007. A marriage of rely/guarantee and separation logic. In Proceedings of the International Conference on Concurrency Theory (CONCUR’07).

Digital Library

[83]

Niki Vazou. 2016. LiquidHaskell: Verification of Haskell Programs with SMTs. Retrieved from http://cufp.org/2016/t6-niki-vazou-liquid-haskell-intro.html.

[84]

Niki Vazou, Alexander Bakst, and Ranjit Jhala. 2015. Bounded refinement types. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’15).

Digital Library

[85]

Niki Vazou, Patrick Rondon, and Ranjit Jhala. 2013. Abstract refinement types. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’13).

Digital Library

[86]

Niki Vazou, Eric L. Seidel, and Ranjit Jhala. 2014a. LiquidHaskell: Experience with refinement types in the real world. In Haskell Workshop.

Digital Library

[87]

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014b. Refinement types for haskell. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP’14).

Digital Library

[88]

John Wickerson, Mike Dodds, and Matthew Parkinson. 2010. Explicit stabilisation for modular rely-guarantee reasoning. In Proceedings of the European Symposium on Programing Languages and Systems (ESOP’10).

Digital Library

[89]

Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kiezun, and Michael D. Ernst. 2007. Object and reference immutability using java generics. In Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC-FSE’07).

Digital Library

[90]

Yoav Zibin, Alex Potanin, Paley Li, Mahmood Ali, and Michael D. Ernst. 2010. Ownership and immutability in generic java. In Proceedings of the ACM International Object Oriented Programming Systems Languages and Applications (OOPSLA’10).

Digital Library

Cited By

Toman JSiqi RSuenaga KIgarashi AKobayashi N(2020)ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative ProgramsProgramming Languages and Systems10.1007/978-3-030-44914-8_25(684-714)Online publication date: 27-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-44914-8_25
Gordon CBergenti FCastegren EDe Koster JFranco J(2019)Modal assertions for actor correctnessProceedings of the 9th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control10.1145/3358499.3361221(11-20)Online publication date: 22-Oct-2019
https://dl.acm.org/doi/10.1145/3358499.3361221
Molina FCornejo CDegiovanni RRegis GCastro PAguirre NFrias M(2019)An evolutionary approach to translating operational specifications into declarative specificationsScience of Computer Programming10.1016/j.scico.2019.05.006181(47-63)Online publication date: Jul-2019
https://doi.org/10.1016/j.scico.2019.05.006
Show More Cited By

Index Terms

Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types
1. Computing methodologies
  1. Concurrent computing methodologies
    1. Concurrent programming languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures
    2. Program reasoning
      1. Invariants
      2. Program verification

Recommendations

Rely-guarantee references for refinement types over aliased mutable data
PLDI '13

Reasoning about side effects and aliasing is the heart of verifying imperative programs. Unrestricted side effects through one reference can invalidate assumptions about an alias. We present a new type system approach to reasoning about safe assumptions ...
Rely-guarantee references for refinement types over aliased mutable data
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation

Reasoning about side effects and aliasing is the heart of verifying imperative programs. Unrestricted side effects through one reference can invalidate assumptions about an alias. We present a new type system approach to reasoning about safe assumptions ...
Alone together: compositional reasoning and inference for weak isolation

Serializability is a well-understood correctness criterion that simplifies reasoning about the behavior of concurrent transactions by ensuring they are isolated from each other while they execute. However, enforcing serializable isolation comes at a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 39, Issue 3

September 2017

196 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/3092741

Editor:
Andrew Myers
Cornell University, USA

Issue’s Table of Contents

Copyright © 2017 ACM.

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 the author(s) 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: 10 May 2017

Accepted: 01 January 2017

Revised: 01 November 2016

Received: 01 August 2015

Published in TOPLAS Volume 39, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

University of Washington, Samsung Research America, and Drexel University

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
476
Total Downloads

Downloads (Last 12 months)127
Downloads (Last 6 weeks)16

Reflects downloads up to 11 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Toman JSiqi RSuenaga KIgarashi AKobayashi N(2020)ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative ProgramsProgramming Languages and Systems10.1007/978-3-030-44914-8_25(684-714)Online publication date: 27-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-44914-8_25
Gordon CBergenti FCastegren EDe Koster JFranco J(2019)Modal assertions for actor correctnessProceedings of the 9th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control10.1145/3358499.3361221(11-20)Online publication date: 22-Oct-2019
https://dl.acm.org/doi/10.1145/3358499.3361221
Molina FCornejo CDegiovanni RRegis GCastro PAguirre NFrias M(2019)An evolutionary approach to translating operational specifications into declarative specificationsScience of Computer Programming10.1016/j.scico.2019.05.006181(47-63)Online publication date: Jul-2019
https://doi.org/10.1016/j.scico.2019.05.006
Kuru IGordon C(2019)Safe Deferred Memory Reclamation with TypesProgramming Languages and Systems10.1007/978-3-030-17184-1_4(88-116)Online publication date: 6-Apr-2019
https://doi.org/10.1007/978-3-030-17184-1_4
Anisetti MArdagna CDamiani EPolegri G(2018)Test-Based Security Certification of Composite ServicesACM Transactions on the Web10.1145/326746813:1(1-43)Online publication date: 4-Dec-2018
https://dl.acm.org/doi/10.1145/3267468
Anisetti MArdagna CGaudenzi FDamiani EDiomede NTufarolo P(2018)Moon Cloud: A Cloud Platform for ICT Security Governance2018 IEEE Global Communications Conference (GLOBECOM)10.1109/GLOCOM.2018.8647247(1-7)Online publication date: 9-Dec-2018
https://dl.acm.org/doi/10.1109/GLOCOM.2018.8647247

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents