Toggle Main Menu Toggle Search

Open Access padlockePrints

Concurrency oracles for free

Lookup NU author(s): Georgy Lukyanov, Dr Andrey Mokhov



This is the final published version of a conference proceedings (inc. abstract) that has been published in its final definitive form by CEUR-WS, 2018.

For re-use rights please refer to the publisher's terms and conditions.


This paper presents an approach to deriving concurrency oracles for processor instructions whose behaviour is formally specified using a state transformer semantics. The presented approach does not require any modification of the existing semantics, nor does it rely on writing a parser for the language in which the semantics is described, thus justifying the “for free” part of the title. The main tool in our arsenal is ad-hoc polymorphism: the presented approach is only applicable when the semantics of processor instructions is expressed using state transformation functions that can be reinterpreted in different contexts. As we show in the paper, such semantics can be interpreted not only for instruction simulation or verification, but also for extracting the information about instruction dependencies, thus allowing us to identify concurrency as well as various types of conflicts between instructions or blocks of instructions.

Publication metadata

Author(s): Lukyanov G, Mokhov A

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: International Workshop on Algorithms & Theories for the Analysis of Event Data (ATAED 2018)

Year of Conference: 2018

Pages: 112-127

Online publication date: 25/06/2018

Acceptance date: 02/04/2018

Date deposited: 11/07/2018

ISSN: 1613-0073

Publisher: CEUR-WS


Series Title: CEUR Workshop Proceedings


Find at Newcastle University icon    Link to this publication