Promising Compilation to ARMv8 POP

A. Podkopaev; Lahav O.; Vafeiadis V.

doi:10.4230/LIPIcs.ECOOP.2017.22

Publications

?

Promising Compilation to ARMv8 POP

Ch. 22. P. 1–28.

Podkopaev A., Lahav O., Vafeiadis V.

In press

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 accesses; however, they do so in rather different ways. Our proof of compilation correctness to ARMv8 POP strengthens the results of the Kang et al., who only proved the correctness of compilation to x86-TSO and Power, which are much simpler in comparison to ARMv8 POP.

Keywords: ARM Compilation Correctness Weak Memory Models

In book

31st European Conference on Object-Oriented Programming, {ECOOP} 2017

Vol. 74. , Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2017.

A Survey of Programming Language Memory Models

Моисеенко Е. А., 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

Making Weak Memory Models Fair

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

Repairing and mechanising the JavaScript relaxed memory model

Watt C., Pulte C., Podkopaev A. et al., , in: PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation.: NY: Association for Computing Machinery (ACM), 2020. P. 346–361.

Added: August 19, 2020

Operational Aspects of C/C++ Concurrency

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

Performance of MD-Algorithms on hybrid systems-on-chip Nvidia Tegra K1 & X1

Nikolskiy V., Vecher V., Stegailov V., , in: Supercomputing. RuSCDays 2016. Communications in Computer and Information Science. Revised Selected Papers.Vol. 687.: Springer, 2016. P. 199–211.

In this paper we consider the efficiency of hybrid systemson-a-chip for high-performance calculations. Firstly, we build Roofline performance models for the systems considered using Empirical Roofline Toolkit and compare the results with the theoretical estimates. Secondly, we use LAMMPS as an example of the molecular dynamic package to demonstrate its performance and efficiency in various ...

Added: May 31, 2017

Verification of MCU-Based Systems Software on an SDVRP Platform

Shershakov S., , in: Proceedings of the International Conference on Electrical and Computer Systems ICECS'12.: Ottawa: International ASET Inc, 2012. P. 207-1–207-8.

The SLAM-based Static Driver Verifier Research Platform (SDVRP), as a tool that systematically analyzes source code and allows writing custom SLIC rules for various platforms, provided a potent verification mechanism for an embedded software system based on ARM Cortex-M0 microprocessor. The correctness of this software is of particular importance in the sense that there are ...

Added: March 14, 2013