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

Gordon, Colin S., Ernst, Michael D., Grossman, Dan, Parkinson, Matthew J.

ACM Transactions on Programming Languages and Systems (TOPLAS), volume 39, number 3, July 2017, doi: 10.1145/3064850

Abstract

We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive enough to accommodate several standard benchmarks with only minor workarounds. The invariants enforced by the types enable an ahead-of-time compiler to carry out optimizations typically beyond the reach of static compilers for dynamic languages. Unlike previous inference techniques for prototype inheritance, our algorithm uses a combination of lower and upper bound propagation to infer types and discover type errors in all code, including uninvoked functions. The inference is expressed in a simple constraint language, designed to leverage off-the-shelf fixed point solvers. We prove soundness for both the type system and inference algorithm. An experimental evaluation showed that the inference is powerful, handling the aforementioned benchmarks with no manual type annotation, and that the inferred types enable effective static compilation.

Bibtex

@article{toplas17,
  abbr = {TOPLAS},
  author = {Gordon, Colin S. and Ernst, Michael D. and Grossman, Dan and Parkinson, Matthew J.},
  title = {{Verifying Invariants of Lock-free Data Structures with Rely-Guarantee and Refinement
      Types}},
  year = {2017},
  journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume={39},
  number={3},
  url = {http://doi.acm.org/10.1145/3064850},
  doi = {10.1145/3064850},
  month = {July},
  note = "2016 Impact Factor (JCR): 3.033.",
  abstract = {
We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive enough to accommodate several standard benchmarks with only minor workarounds. The invariants enforced by the types enable an ahead-of-time compiler to carry out optimizations typically beyond the reach of static compilers for dynamic languages. Unlike previous inference techniques for prototype inheritance, our algorithm uses a combination of lower and upper bound propagation to infer types and discover type errors in all code, including uninvoked functions. The inference is expressed in a simple constraint language, designed to leverage off-the-shelf fixed point solvers. We prove soundness for both the type system and inference algorithm. An experimental evaluation showed that the inference is powerful, handling the aforementioned benchmarks with no manual type annotation, and that the inferred types enable effective static compilation.
  },
  pdf = {papers/toplas17.pdf},
  slides = {papers/toplas17pldi17_slides.pdf},
  acm = {http://doi.acm.org/10.1145/3064850},
  youtube = {https://youtu.be/dar-mVn5N8U},
  code = {https://github.com/csgordon/rgref-concurrent},
  bibtex_show = {true},
  morecode = {https://github.com/csgordon/rghaskell}
}