EMME: a formal tool for ECMAScript Memory Model Evaluation

EMME: a formal tool for ECMAScript Memory Model Evaluation” by Cristian Mattarei, Clark Barrett, Shu-yu Guo, Bradley Nelson, and Ben Smith. In Proceedings of the 24^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '18), (Dirk Beyer and Marieke Huisman, eds.), Apr. 2018, pp. 55-71. Thessaloniki, Greece. Distinguished Artifact Award..

Abstract

Nearly all web-based interfaces are written in JavaScript. Given its prevalence, the support for high performance JavaScript code is crucial. The ECMA Technical Committee 39 (TC39) has recently extended the ECMAScript language (i.e., JavaScript) to support shared memory accesses between different threads. The extension is given in terms of a natural language memory model specification. In this paper we describe a formal approach for validating both the memory model and its implementations in various JavaScript engines. We first introduce a formal version of the memory model and report results on checking the model for consistency and other properties. We then introduce our tool, EMME, built on top of the Alloy analyzer, which leverages the model to generate all possible valid executions of a given JavaScript program. Finally, we report results using EMME together with small test programs to analyze industrial JavaScript engines. We show that EMME can find bugs as well as missed opportunities for optimization.

BibTeX entry:

@inproceedings{MBG+18,
   author = {Cristian Mattarei and Clark Barrett and Shu-yu Guo and
	Bradley Nelson and Ben Smith},
   editor = {Dirk Beyer and Marieke Huisman},
   title = {{EMME}: a formal tool for {ECMAS}cript Memory Model Evaluation},
   booktitle = {Proceedings of the {\it 24^{th}} International Conference
	on Tools and Algorithms for the Construction and Analysis of
	Systems (TACAS '18)},
   series = {Lecture Notes in Computer Science},
   volume = {10806},
   pages = {55--71},
   publisher = {Springer},
   month = apr,
   year = {2018},
   isbn = {978-3-319-89963-3},
   doi = {10.1007/978-3-319-89963-3_4},
   note = {Thessaloniki, Greece. {\em Distinguished Artifact Award.}},
   url = {http://theory.stanford.edu/~barrett/pubs/MBG+18.pdf}
}

(This webpage was created with bibtex2web.)