About The Forum
Calendar 2017 Poster Sessions : SMT-based Formal Analysis of the ECMAScript Shared Memory Model
Student Name : Cristian Mattarei
Advisor : None
Advisor : None
Abstract:
JavaScript represents over 90% of the languages used to define web-based front-end interfaces. Given such a broad distribution, the support of advanced functionalities to guarantee high level of performance is fundamental. ECMA is the industry association oriented to standardize the ECMAScript programming language (i.e., JavaScript), and its Technical Committee 39 (TC39) is currently in the process of extending the language with the support of shared memory. This extension will improve the performance of multithread programs, and give a more efficient support to multiprocessors and multicores systems.
Every extension of the JavaScript language requires to be specified with a well defined semantics, and in the case of shared memory operations, this requirement is covered by an axiomatic memory model. More specifically, a memory model consists in a set of constraints that must be satisfied in order to identify a valid program execution. The set of executions that satisfy those constraints is finite, and they represent all possible valid program interpretations.
In this work we provide an automated approach to extract all valid memory model interpretations. The proposed technique consists in formalize both the axiomatic memory model and a representation of the candidate JavaScript program into Satisfiability Modulo Theories (SMT). This formal representation can be then analyzed via an SMT-solver (i.e., CVC4), which provides all possible models of the formula i.e., a representation of the set of valid memory model interpretations.
Bio:
Cristian Mattarei is a postdoctoral researcher at Stanford University, working on SAT and SMT based formal verification techniques. Cristian received his PhD in Information and Communication Technology, from University of Trento and Fondazione Bruno Kessler (Italy) in 2016. His research interests comprise BDD, SAT, and SMT based formal verification, symbolic model checking, model-based safety and reliability analyses, formal contract-based design, and formal modeling.
JavaScript represents over 90% of the languages used to define web-based front-end interfaces. Given such a broad distribution, the support of advanced functionalities to guarantee high level of performance is fundamental. ECMA is the industry association oriented to standardize the ECMAScript programming language (i.e., JavaScript), and its Technical Committee 39 (TC39) is currently in the process of extending the language with the support of shared memory. This extension will improve the performance of multithread programs, and give a more efficient support to multiprocessors and multicores systems.
Every extension of the JavaScript language requires to be specified with a well defined semantics, and in the case of shared memory operations, this requirement is covered by an axiomatic memory model. More specifically, a memory model consists in a set of constraints that must be satisfied in order to identify a valid program execution. The set of executions that satisfy those constraints is finite, and they represent all possible valid program interpretations.
In this work we provide an automated approach to extract all valid memory model interpretations. The proposed technique consists in formalize both the axiomatic memory model and a representation of the candidate JavaScript program into Satisfiability Modulo Theories (SMT). This formal representation can be then analyzed via an SMT-solver (i.e., CVC4), which provides all possible models of the formula i.e., a representation of the set of valid memory model interpretations.
Bio:
Cristian Mattarei is a postdoctoral researcher at Stanford University, working on SAT and SMT based formal verification techniques. Cristian received his PhD in Information and Communication Technology, from University of Trento and Fondazione Bruno Kessler (Italy) in 2016. His research interests comprise BDD, SAT, and SMT based formal verification, symbolic model checking, model-based safety and reliability analyses, formal contract-based design, and formal modeling.