Please use this identifier to cite or link to this item:
|Title:||Memory model sensitive bytecode verification|
Programming language memory models
Software model checking
|Citation:||Huynh, T.Q., Roychoudhury, A. (2007). Memory model sensitive bytecode verification. Formal Methods in System Design 31 (3) : 281-305. ScholarBank@NUS Repository. https://doi.org/10.1007/s10703-007-0041-6|
|Abstract:||Modern concurrent programming languages like C# and Java have a programming language level memory model, which captures the set of all allowed behaviors of programs on any implementation platform-uni- or multi-processor. Such a memory model is typically weaker than Sequential Consistency and allows reordering of operations within a program thread. Therefore, programs verified correct by assuming Sequential Consistency (that is, each thread proceeds in program order) may not behave correctly on certain platforms! One solution to this problem is to develop program checkers which are memory model sensitive. In this paper, we develop a bytecode level invariant checker for the programming language C#. Our checker identifies program states which are reached only because the C# memory model is more relaxed than Sequential Consistency. It employs partial order reduction strategies to speed up the search. These strategies are different from standard partial order reduction methods since our search also considers execution traces containing bytecode re-orderings. Furthermore, our checker identifies (a) operation re-orderings which cause undesirable states to be reached, and (b) simple program modifications-by inserting memory barrier operations-which prevent such undesirable re-orderings. © 2007 Springer Science+Business Media, LLC.|
|Source Title:||Formal Methods in System Design|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Jun 15, 2018
WEB OF SCIENCETM
checked on May 15, 2018
checked on Jun 2, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.