pizlonator
commented
7 years ago I fear that the approach being taken here is too complicated to allow for meaningful scrutiny. Good luck having experts review the binary relations in SMT-LIB.
Open jfbastien opened 8 years ago
pizlonator
commented
7 years ago I fear that the approach being taken here is too complicated to allow for meaningful scrutiny. Good luck having experts review the binary relations in SMT-LIB.
pizlonator
commented
7 years ago Sorry, I was missing context. I now see that this is a proposal to verify this model (https://github.com/tc39/ecmascript_sharedmem/blob/llvm-like/LLVM_LIKE.md) and potentially extend it.
I think it makes sense to have a prose model, and that the LLVM_LIKE model is a sensible starting point. I also think it makes sense to formally verify that model.
asajeffrey
commented
7 years ago @pizlonator a first shot at formalizing the llvm-like model is at https://github.com/asajeffrey/ecmascript_sharedmem/blob/master/MEMMODEL_WIP.md. There are still some discrepancies between the two models, and we're not yet in a theorem prover, but it will hopefully be steps in the right direction.
As discussed in #88, it is desirable to have a formal memory model for SharedArrayBuffer. We've secured funding for such a project, and will be pursuing it over the next year.
This issue tracks the progress, and points to relevant outside resources pertaining to this work.
Below is an outline of the intended work.
Please file dependent issues if you have questions / suggestions about the research itself, or redirect them to the appropriate outside repositories. This is merely a tracking bug!
Project
Title: JavaScript SharedArrayBuffer / WebAssembly threading formal memory model Institution Name: Stanford Principal Investigator Name: Clark Barrett
Abstract
As processor development moves from faster clock speeds to more cores, leveraging concurrency is becoming increasingly important. It is well-known, however, that concurrency adds a significant level of complexity to programs. Thus, many efforts are underway to make it easier and safer to develop and reason about concurrent programs. Notable efforts include, for example, the standardization of a memory model for C++.
Because reasoning about concurrency, especially in the presence of relaxed memory models, is highly counterintuitive, this is an area where formal approaches can have (and have had) a significant impact. A new effort is now underway, in collaboration with all major browser vendors, to add support for threads to JavaScript and WebAssembly. The potential benefits are enormous, but the possibility for error is also great. For this reason, we propose taking a systematic, formal approach to analyzing and (where possible) verifying the new memory model.
Description
All major browser vendors are adding support for threads+atomic to JavaScript and WebAssembly. We’ve received significant enthusiasm from game studios and high performance developers: these features are highly desirable to supporting their applications efficiently on the web.
Writing such code is fraught with peril because human intuition is extremely error-prone when reasoning about how hardware executes high-level languages across multiple cores. Specifying a memory model for this execution is yet more difficult and gets even more complex when considering portability: for instance, V8 currently supports 9 hardware Instruction Set Architectures. The virtual ISA which browsers define must map correctly and efficiently to each of these hardware ISAs; anything less defeats the performance and portability goals of the feature. An erroneous specification leads to unexpected and hard-to-reproduce behavior on some platforms, making it impossible to write multithreaded code correctly for the web. We’re at a point in the design process where using formal methods to specify the memory model would be tremendously helpful to provably ensure correctness and portability. The specification is currently English prose and has been reviewed by multiple domain experts, but experience tells us it’s likely flawed in interesting cases.
A similar effort to formally reason about the C++ memory model led to the discovery of many issues that were subsequently fixed. Mark Batty’s dissertation describing this work won two major awards†. Formal models have also been used to analyze hardware ISAs (e.g. Jade Alglave’s thesis‡), but to date, this kind of analysis has never been done for a virtual ISA. Formally analyzing the new memory model will thus be a challenging research task. At the same time, the potential benefits of a robust memory model are tremendous.
Goals & Methodology
The most intuitive model for concurrency is the Sequential Consistency (SC) model introduced by Leslie Lamport back in 1979§. This model requires that all events in a concurrent execution happen in such a way that the result is equivalent to some interleaving of the individual events in each thread. Unfortunately SC is too restrictive for modern performance requirements, and so modern hardware allows for various relaxations of SC. For example, a processor may read a value that was written (by the same processor) earlier, even though that written value has not yet made it to main memory (this happens, for example, when reads from a store buffer are allowed).
Jade Alglave’s PhD thesis provides a theoretical foundation for reasoning about and axiomatizing relaxed memory models. She uses binary relations which are partial orders to model relationships between memory events. For example, the
wsrelation between two writes has the property thatws(w1,w2)iffw1occurs beforew2in the global timeline. Using a number of different relations, one can specify which aspects of a particular model follow SC and which are relaxed.A particularly appealing feature of this axiomatic approach is that it can be used to drive test generation. For each “axiom” (i.e. each additional relational property that is assumed to hold on events in the model), one can generate small litmus tests for the axiom as follows. Assume the other axioms hold, and then find a small test case satisfying these axioms but falsifying the axiom under analysis. In fact, this process can be automated by using an automated reasoning tool. This same theoretical foundation was used to analyze the C++ memory model.
We plan to take a similar approach for the JavaScript memory model. We will first review the literature and results for hardware models and the C++ model. We will then go through the JavaScript specification and translate it into a relational model. Depending on the features of the model, this may require some significant innovation. However, we are confident that a first-order language will be sufficient to capture the axioms of the model.
Next, we will use an automated reasoning tool to generate litmus tests as described above. One tool that has already been shown to be very effective is Alloy‖, a tool built on top of Boolean satisfiability (SAT) technology which presents a nice relational interface to the user. In addition, we will experiment with using the CVC4¶ solver for satisfiability modulo theories (SMT). Like other SMT solvers, CVC4 is based on the DPLL(T) architecture which combines a fast SAT solver with custom theory reasoners. This architecture has been shown to be more powerful and scalable (on some problems) than a purely SAT-based approach. However, unlike other SMT solvers, CVC4 has native theory reasoning support for sets and relations. This makes CVC4 an ideal candidate for relational reasoning.
Finally, we will explore whether some aspects of the memory model can be proved to be correct, either in isolation, or with respect to some implementation on a particular hardware ISA. This will require formulating certain desirable properties of the memory model formally and then proving them, again most likely leveraging an automated tool such as an SMT solver.
Deliverables
References
† Batty, M., The C11 and C++11 Concurrency Model. PhD Thesis, University of Cambridge, 2014. ‡ Alglave, J., A Shared Memory Poetics. PhD Thesis, University of Paris 7 - Diderot, 2010. § Lamport, L., How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Comput., 46(7):779–782, 1979. ‖ Jackson, D., Alloy: A Lightweight Object Modelling Notation. ACM TOSEM, 11(2):256–290, 2002. ¶ Barrett, C. et al., CVC4. Proceedings of Computer Aided Verification (CAV), 171-177, 2011.