JavaScript松弛记忆模型的修复和机制化
Repairing and Mechanising the JavaScript Relaxed Memory Model
摘要：
现代JavaScript包括SharedArrayBuffer特性，它提供了对真正的共享内存并发的访问。SharedArrayBuffers是简单的字节线性缓冲区，JavaScript规范定义了一个公理化的宽松内存模型来描述它们的行为。虽然该模型在很大程度上基于C/C++11模型，但它在一些关键领域存在分歧。JavaScript选择为数据竞争提供定义良好的语义，这与C/C++11的“未定义行为”不同。此外，JavaScript模型是混合大小的。这意味着它的访问不是离散的位置，而是（可能重叠的）字节范围。我们表明，该模型，违反了设计意图，不支持编译方案，在实践中使用的ARMv 8。我们提出了一个更正，其中还包括先前提出的修复模型的故障，提供顺序一致性的数据竞争自由程序（SC-DRF），一个重要的正确性条件。我们在Alloy中使用模型检验来生成这些缺陷的小反例，并研究我们的修正。为了实现这一点，我们还开发了一个混合大小的扩展到现有的ARMv 8公理模型。在我们的Alloy实验的指导下，我们（在Coq中）机械化了JavaScript模型（校正和未校正），我们的ARMv 8模型，以及对于校正的JavaScript模型，一个“模型内部”SC-DRF证明和一个编译方案正确性证明到ARMv 8。此外，我们研究了修正后的JavaScript模型的非混合大小子集，并通过中间内存模型（IMM）证明了该子集在x86-TSO，Power，RISC-V，ARMv7和（再次）ARMv 8中的编译正确性。作为我们工作的结果，JavaScript标准机构（ECMA TC 39）将在即将发布的规范版本中包含对这两个问题的修复。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
