?
Repairing and mechanising the JavaScript relaxed memory model
P. 346–361.
Watt C., Pulte C., Podkopaev A., Barbier G., Dolan S., Flur S., Pichon-Pharabod J., Guo S.
In book
NY: Association for Computing Machinery (ACM), 2020.
Моисеенко Е. А., Podkopaev A., Кознов Д. В., Programming and Computer Software 2021 Vol. 47 No. 6 P. 439–456
A memory model defines the semantics of concurrent programs operating on a shared memory. The most well-known and intuitive memory model, sequential consistency, is too strong for modern languages as it forbids many outcomes observable on modern hardware as a result of compiler and CPU optimizations. This gave rise to so-called weak or relaxed memory models. In recent years dozens of (weak) ...
Added: February 2, 2022
Lahav O., Namakonov E., Oberhauser J. et al., Proceedings of the ACM on Programming Languages 2021 Vol. 5 No. OOPSLA Article 98
Liveness properties, such as termination, of even the simplest shared-memory concurrent programs under sequential consistency typically require some fairness assumptions about the scheduler. Under weak memory models, we observe that the standard notions of thread fairness are insufficient, and an additional fairness property, which we call memory fairness, is needed. In this paper, we propose ...
Added: February 2, 2022
Starikov S., Kolotova L., Scripta Materialia 2016 Vol. 113 P. 27–30
Using molecular dynamics simulations, we study the structural properties of body-centered cubic (BCC) and
body-centered tetragonal (BCT) phases of U–Mo alloys. The local positions of uranium atoms in the BCC phase
correspond to the BCT structure. Thus, the BCC lattice exhibits cubic symmetry only on the scale of several
interatomic spacings, and it is therefore more correct to ...
Added: January 28, 2022
Grigorev S., Bozhko S., Хатбуллина Л. Р., Lecture Notes in Computer Science 2019 Vol. 11541 P. 264–281
Formal language theory has a deep connection with such areas as static code analysis, graph database querying, formal verifica- tion, and compressed data processing. Many application problems can be formulated in terms of languages intersection. The Bar-Hillel theo- rem states that context-free languages are closed under intersection with a regular set. This theorem has a ...
Added: August 20, 2019
Podkopaev A., Sergey I., Nanevski A., / Series Computer Science "arxiv.org". 2016.
In this work, we present a family of operational semantics that gradually approximates the realistic program behaviors in the C/C++11 memory model. Each semantics in our framework is built by elaborating and combining two simple ingredients: viewfronts and operation buffers. Viewfronts allow us to express the spatial aspect of thread interaction, i.e., which values a ...
Added: December 24, 2018
Podkopaev A., Lahav O., Vafeiadis V., , in: 31st European Conference on Object-Oriented Programming, {ECOOP} 2017Vol. 74.: Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2017. Ch. 22 P. 1–28.
We prove the correctness of compilation of relaxed memory accesses and release-acquire fences from the "promising" semantics of [Kang et al. POPL'17] to the ARMv8 POP machine of [Flur et al. POPL'16]. The proof is highly non-trivial because both the ARMv8 POP and the promising semantics provide some extremely weak consistency guarantees for normal memory ...
Added: December 24, 2018