An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors

Kathryn Gray, Gabriel Kerneis, Dominic Mulligan, Christopher Pulte, Susmit Sarkar, Peter Sewell

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Citations (Scopus)
3 Downloads (Pure)

Abstract

Weakly consistent multiprocessors such as ARM and IBM POWER have been with us for decades, but their subtle programmer-visible concurrency behaviour remains challenging, both to implement and to use; the traditional architecture documentation, with its mix of prose and pseudocode, leaves much unclear.
In this paper we show how a precise architectural envelope model for such architectures can be defined, taking IBM POWER as our example. Our model specifies, for an arbitrary test program, the set of all its allowable executions, not just those of some particular implementation. The model integrates an operational concurrency model with an ISA model for the fixedpoint
non-vector user-mode instruction set (largely automatically derived from the vendor pseudocode, and expressed in a new ISA description language). The key
question is the interface between these two: allowing all the required concurrency behaviour, without overcommitting to some particular microarchitectural implementation, requires a novel abstract structure. Our model is expressed in a mathematically rigorous language that can be automatically translated to an executable test-oracle tool; this lets one either interactively explore or exhaustively compute the set of all allowed behaviours of intricate test cases, to provide a reference for hardware and software development.
Original languageEnglish
Title of host publicationMICRO-48 Proceedings of the 48th International Symposium on Microarchitecture
Place of PublicationNew York
PublisherACM
Pages635-646
ISBN (Print)9781450340342
DOIs
Publication statusPublished - 5 Dec 2015
EventThe 48th International Symposium on Microarchitecture, 2015 MICRO-48 - Hilton Hawaiian Village, Waikiki, Hawaii, United States
Duration: 5 Dec 20159 Dec 2015
http://www.microarch.org/micro48/

Conference

ConferenceThe 48th International Symposium on Microarchitecture, 2015 MICRO-48
Country/TerritoryUnited States
CityWaikiki, Hawaii
Period5/12/159/12/15
Internet address

Fingerprint

Dive into the research topics of 'An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors'. Together they form a unique fingerprint.

Cite this