• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • Promising Compilation to ARMv8 POP
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
October 30, 2026
‘This Format Turned Each Presentation Into a Collaborative Effort to Assess the Robustness of the Study
On October 16, 2026, HSE ICEF hosted the Eighth International Conference on Applied Economics. Held fully on-site, the conference brought researchers from HSE University, the New Economic School, Wuhan University, and Shandong University together in Moscow. The programme was organised around three overarching themes— ‘Environment, Resources and Policy,’ ‘Migration, Labour, and Communication,’ and ‘Consumption, Behaviour, and Climate—offering an opportunity to see how similar economic mechanisms operate in China, Pakistan, the United States, and Russia.
October 23, 2026
‘I Always Conduct Research on Topics That Genuinely Matter to Me
Anastasiia Deeva studies the socio-economic consequences of excess weight in Russia. In an interview for the Young Scientists of HSE University project, she spoke about why beauty cannot be measured, her desire to write a novel, ‘Dostoevskian’ burnout, and working at the hotel where The Shining was filmed.
October 19, 2026
'Cultural Studies Seeks to Understand What Lies Beneath the Surface of Everyday Things'
Maxim Zhiganov has been exploring different aspects of sound for many years—first in relation to his native Perm and then on a broader, global scale. In this interview for the HSE Young Scientists project, he talks about sound maps, the special issue of the journal Logos, and why it is important to make the familiar less clear and obvious.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

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.

Language: English
Full text
DOI
Text on another site
Keywords: ARMCompilation CorrectnessWeak Memory Models

In book

31st European Conference on Object-Oriented Programming, {ECOOP} 2017
Vol. 74. , Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2017.
Similar publications
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
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit