Mixed-Size Concurrency: ARM, POWER, C/C++11, and SC
| Autor: | Susmit Sarkar, Peter Sewell, Mark Batty, Christopher Pulte, Kyndylan Nienhuis, Ali Sezgin, Luc Maranget, Shaked Flur, Kathryn E. Gray |
|---|---|
| Přispěvatelé: | University of Cambridge [UK] (CAM), University of St Andrews [Scotland], Langages de programmation, types, compilation et preuves (GALLIUM), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), University of Kent [Canterbury], ACM, ANR-05-BDIV-0011,REMIGE,Réponses comportementales et démographiques des prédateurs marins de l'Océan Indien aux changements globaux(2005), Fluet, Matthew, University of St Andrews. School of Computer Science |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
QA75
Computer science Semantics (computer science) QA75 Electronic computers. Computer science Concurrency NDAS 02 engineering and technology ISA computer.software_genre 01 natural sciences Software F31 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs Keywords Relaxed Memory Models mixed-size 0103 physical sciences 0202 electrical engineering electronic engineering information engineering Code (cryptography) semantics R2C 010302 applied physics [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] business.industry Sequential consistency Programming language C0 [General]: Modeling of computer architecture ~DC~ Mixed-size 020207 software engineering Computer Graphics and Computer-Aided Design Memory barrier Semantics 020202 computer hardware & architecture Allocator Relaxed Memory Models BDC business computer D13 [Programming Techniques]: Con- current Programming—Parallel programming |
| Zdroj: | 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), ACM, Jan 2017, Paris, France POPL |
| ISSN: | 0362-1340 |
| Popis: | This work was partly funded by the EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems, EP/K008528/1, EPSRC grant C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence EP/M027317/1 (Sarkar), an ARM iCASE award (Pulte), a Gates Cambridge Scholarship (Nienhuis). and ANR grant WMC (ANR-11-JS02-011, Maranget). Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store. In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level. A semantic foundation for software, therefore, has to address them. We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff. This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting. In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency. We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses. This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests. Postprint |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|