Repairing and mechanising the JavaScript relaxed memory model
Repairing and mechanising the JavaScript relaxed memory model
复制标题
修复和机械化 JavaScript 宽松内存模型
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Shu
中科院分区：
文献类型：
--
作者：
Conrad Watt;Christopher Pulte;A. Podkopaev;G. Barbier;Stephen Dolan;Shaked Flur;Jean Pichon;Shu
Modern JavaScript包括共享arraybuffer功能，可访问对真实共享内存并发。共享arrayBuffer是字节的简单线性缓冲区，JavaScript规范定义了一个公理放松的内存模型来描述其行为。尽管该模型基于C/C ++ 11模型，但它在某些关键领域有所不同。 JavaScript选择为数据率提供明确定义的语义，这与C/C ++ 11的“未定义行为”不同。此外，JavaScript模型是混合尺寸的。这意味着它的访问不是离散位置，而是（可能重叠）字节范围。我们表明，该模型违反了设计意图，不支持用于实践中使用的ARMV8的汇编方案。我们提出了一个校正，该校正还包含了先前提出的修复模型未能提供无数据率程序（SC-DRF）的一致性的修复程序，这是一个重要的正确性条件。我们在合金中使用模型检查来为这些缺陷生成小型反例，并研究我们的校正。为此，我们还为现有的ARMV8公理模型开发了混合尺寸扩展。在我们的合金实验的指导下，我们（在COQ中）JavaScript模型（校正和未校正），我们的ARMV8模型，以及用于校正后的JavaScript模型，“模型内部” SC-DRF证明和汇编方案的正确性证明，以证明对ARMV8。此外，我们研究了校正后的JavaScript模型的非混合大小子集，并通过中间存储器提供了该子集的汇编正确性的证明，可为X86-TSO，Power，risc-V，ARMV7和（再次）ARMV8提供证明。模型（IMM）。由于我们的工作，JavaScript标准主体（ECMA TC39）将在即将到来的规范版本中涵盖这两个问题的修复程序。
Modern JavaScript includes the SharedArrayBuffer feature, which provides access to true shared memory concurrency. SharedArrayBuffers are simple linear buffers of bytes, and the JavaScript specification defines an axiomatic relaxed memory model to describe their behaviour. While this model is heavily based on the C/C++11 model, it diverges in some key areas. JavaScript chooses to give a well-defined semantics to data-races, unlike the "undefined behaviour" of C/C++11. Moreover, the JavaScript model is mixed-size. This means that its accesses are not to discrete locations, but to (possibly overlapping) ranges of bytes. We show that the model, in violation of the design intention, does not support a compilation scheme to ARMv8 which is used in practice. We propose a correction, which also incorporates a previously proposed fix for a failure of the model to provide Sequential Consistency of Data-Race-Free programs (SC-DRF), an important correctness condition. We use model checking, in Alloy, to generate small counter-examples for these deficiencies, and investigate our correction. To accomplish this, we also develop a mixed-size extension to the existing ARMv8 axiomatic model. Guided by our Alloy experimentation, we mechanise (in Coq) the JavaScript model (corrected and uncorrected), our ARMv8 model, and, for the corrected JavaScript model, a "model-internal" SC-DRF proof and a compilation scheme correctness proof to ARMv8. In addition, we investigate a non-mixed-size subset of the corrected JavaScript model, and give proofs of compilation correctness for this subset to x86-TSO, Power, RISC-V, ARMv7, and (again) ARMv8, via the Intermediate Memory Model (IMM). As a result of our work, the JavaScript standards body (ECMA TC39) will include fixes for both issues in an upcoming edition of the specification.
登录
查看更多内容
DOI：
10.1145/2837614.2837615
发表时间：
2016-01
期刊：
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
通讯作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
同步 C/C 和 POWER
DOI：
10.1145/2254064.2254102
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S
DOI：
10.1145/3009837.3009838
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Wickerson J
通讯作者：
Wickerson J
值得信赖的机械化 JavaScript 规范
DOI：
10.1145/2535838.2535876
发表时间：
2014
期刊：
--
影响因子：
--
作者：
Bodin M
通讯作者：
Bodin M
混合大小并发：ARM、POWER、C/C 11 和 SC
DOI：
10.1145/3009837.3009839
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Flur S
通讯作者：
Flur S