TY - GEN
T1 - TransForm
T2 - 47th ACM/IEEE Annual International Symposium on Computer Architecture, ISCA 2020
AU - Hossain, Naorin
AU - Trippel, Caroline
AU - Martonosi, Margaret
N1 - Publisher Copyright:
© 2020 IEEE.
PY - 2020/5
Y1 - 2020/5
N2 - Memory consistency models (MCMs) specify the legal ordering and visibility of shared memory accesses in a parallel program. Traditionally, instruction set architecture (ISA) MCMs assume that relevant program-visible memory ordering behaviors only result from shared memory interactions that take place between user-level program instructions. This assumption fails to account for virtual memory (VM) implementations that may result in additional shared memory interactions between user-level program instructions and both 1) system-level operations (e.g., address remappings and translation lookaside buffer invalidations initiated by system calls) and 2) hardware-level operations (e.g., hardware page table walks and dirty bit updates) during a user-level program' s execution. These additional shared memory interactions can impact the observable memory ordering behaviors of user-level programs. Thus, memory transistency models (MTMs) have been coined as a superset of MCMs to additionally articulate VM-aware consistency rules. However, no prior work has enabled formal MTM specifications, nor methods to support their automated analysis. To fill the above gap, this paper presents the TransForm framework. First, TransForm features an axiomatic vocabulary for formally specifying MTMs. Second, TransForm includes a synthesis engine to support the automated generation of litmus tests enhanced with MTM features (i.e., enhanced litmus tests, or ELTs) when supplied with a TransForm MTM specification. As a case study, we formally define an estimated MTM for Intel x86 processors, called x86t-elt, that is based on observations made by an ELT-based evaluation of an Intel x86 MTM implementation from prior work and available public documentation [23], [29]. Given x86t-elt and a synthesis bound (on program size) as input, TransForm' s synthesis engine successfully produces a complete set of ELTs (within a 9-instruction bound) including relevant hand-curated ELTs from prior work, plus 100 more.
AB - Memory consistency models (MCMs) specify the legal ordering and visibility of shared memory accesses in a parallel program. Traditionally, instruction set architecture (ISA) MCMs assume that relevant program-visible memory ordering behaviors only result from shared memory interactions that take place between user-level program instructions. This assumption fails to account for virtual memory (VM) implementations that may result in additional shared memory interactions between user-level program instructions and both 1) system-level operations (e.g., address remappings and translation lookaside buffer invalidations initiated by system calls) and 2) hardware-level operations (e.g., hardware page table walks and dirty bit updates) during a user-level program' s execution. These additional shared memory interactions can impact the observable memory ordering behaviors of user-level programs. Thus, memory transistency models (MTMs) have been coined as a superset of MCMs to additionally articulate VM-aware consistency rules. However, no prior work has enabled formal MTM specifications, nor methods to support their automated analysis. To fill the above gap, this paper presents the TransForm framework. First, TransForm features an axiomatic vocabulary for formally specifying MTMs. Second, TransForm includes a synthesis engine to support the automated generation of litmus tests enhanced with MTM features (i.e., enhanced litmus tests, or ELTs) when supplied with a TransForm MTM specification. As a case study, we formally define an estimated MTM for Intel x86 processors, called x86t-elt, that is based on observations made by an ELT-based evaluation of an Intel x86 MTM implementation from prior work and available public documentation [23], [29]. Given x86t-elt and a synthesis bound (on program size) as input, TransForm' s synthesis engine successfully produces a complete set of ELTs (within a 9-instruction bound) including relevant hand-curated ELTs from prior work, plus 100 more.
KW - axiomatic modeling
KW - enhanced litmus tests
KW - memory consistency
KW - memory transistency
KW - synthesis
UR - http://www.scopus.com/inward/record.url?scp=85092009455&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85092009455&partnerID=8YFLogxK
U2 - 10.1109/ISCA45697.2020.00076
DO - 10.1109/ISCA45697.2020.00076
M3 - Conference contribution
AN - SCOPUS:85092009455
T3 - Proceedings - International Symposium on Computer Architecture
SP - 874
EP - 887
BT - Proceedings - 2020 ACM/IEEE 47th Annual International Symposium on Computer Architecture, ISCA 2020
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 30 May 2020 through 3 June 2020
ER -