Please use this identifier to cite or link to this item: https://doi.org/10.1007/s10703-007-0041-6
Title: Memory model sensitive bytecode verification
Authors: Huynh, T.Q.
Roychoudhury, A. 
Keywords: Bytecode verification
Programming language memory models
Software model checking
Issue Date: 2007
Source: 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
URI: http://scholarbank.nus.edu.sg/handle/10635/39828
ISSN: 09259856
DOI: 10.1007/s10703-007-0041-6
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

18
checked on Dec 13, 2017

WEB OF SCIENCETM
Citations

8
checked on Dec 13, 2017

Page view(s)

45
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.