Hardware-Assisted Online Data Race Detection
Chapter, Peer reviewed
Accepted version
Permanent lenke
https://hdl.handle.net/11250/2984243Utgivelsesdato
2021Metadata
Vis full innførselSamlinger
Originalversjon
Ahishakiye, F., Requeno Jarabo, J. I., Pun, K. I., & Stolz, V. (2021). Hardware-assisted online data race detection. In E. Bartocci, Y. Falcone, & M. Leucker (Eds.), Formal methods in outer space: Essays dedicated to Klaus Havelund on the occasion of his 65th birthday (pp. 108-126). 10.1007/978-3-030-87348-6_6Sammendrag
Dynamic data race detection techniques usually involve invasive instrumentation that makes it impossible to deploy an executable with such checking in the field, hence making errors difficult to debug and reproduce. This paper shows how to detect data races using the COEMS technology through continuous online monitoring with low-impact instrumentation on a novel FPGA-based external platform for embedded multicore systems. It is used in combination with formal specifications in the high-level stream-based temporal specification language TeSSLa, in which we encode a lockset-based algorithm to indicate potential race conditions. We show how to instantiate a TeSSLa template that is based on the Eraser algorithm, and present a corresponding light-weight instrumentation mechanism that emits necessary observations to the FPGA with low overhead. We illustrate the feasibility of our approach with experimental results on detection of data races on a sample application.
Beskrivelse
This version of the article has been accepted for publication, after peer review (when applicable) and is subject to Springer Nature’s AM terms of use, but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections. The Version of Record is available online at: https://doi.org/10.1007/978-3-030-87348-6_6