References of "Linden, Alexander"
     in
Bookmark and Share    
Full Text
See detailOn the Verification of Programs on Relaxed Memory Models
Linden, Alexander ULg

Doctoral thesis (2013)

Classical model-checking tools verify concurrent programs under the traditional "Sequential Consistency" (SC) memory model, in which all accesses to the shared memory are immediately visible globally, and ... [more ▼]

Classical model-checking tools verify concurrent programs under the traditional "Sequential Consistency" (SC) memory model, in which all accesses to the shared memory are immediately visible globally, and where model-checking consists in verifying a given property when exploring the state space of a program. However, modern multi-core processor architectures implement relaxed memory models, such as "Total Store Order" (TSO), "Partial Store Order" (PSO), or an extension with locks such as "x86-TSO", which allow stores to be delayed in various ways and thus introduce many more possible executions, and hence errors, than those present in SC. Of course, one can force a program executed in the context of a relaxed memory system to behave exactly as in SC by adding synchronization operations after every memory access. But this totally defeats the performance advantage that is precisely the motivation for implementing relaxed memory models instead of SC. Thus, when moving a program to an architecture implementing a relaxed memory model (which includes most current multi-core processors), it is essential to have tools to help the programmer check if correctness (e.g. a safety property) is preserved and, if not, to minimally introduce the necessary synchronization operations. The proposed verification approach uses an operational store-buffer-based semantics of the chosen relaxed memory models and proceeds by using finite automata for symbolically representing the possible contents of the buffers. Store, load, commit and other synchronization operations then correspond to operations on these finite automata. The advantage of this approach is that it operates on (potentially infinite) sets of buffer contents, rather than on individual buffer configurations, and that it is compatible with partial-order reduction techniques. This provides a way to tame the explosion of the number of possible buffer configurations, while preserving the full generality of the analysis. It is thus possible to even check designs that may contain cycles. This verification approach then serves as a basis to a memory fence insertion algorithm that finds how to preserve the correctness of a program when it is moved from SC to TSO or PSO. Its starting point is a program that is correct for the sequential consistency memory model (with respect to a given safety property), but that might be incorrect under TSO or PSO. This program is then analyzed for the chosen relaxed memory model and when errors are found (a violated safety property), memory fences are inserted in order to avoid these errors. The approach proceeds iteratively and heuristically, inserting memory fences until correctness is obtained, which is guaranteed to happen. [less ▲]

Detailed reference viewed: 67 (13 ULg)
Full Text
Peer Reviewed
See detailA Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems
Linden, Alexander ULg; Wolper, Pierre ULg

in Proceedings of the 19th international conference on Tools and algorithms for the construction and analysis of systems (2013, March)

This paper addresses the problem of verifying and correcting programs when they are moved from a sequential consistency execution environment to a relaxed memory context. Specifically, it considers the ... [more ▼]

This paper addresses the problem of verifying and correcting programs when they are moved from a sequential consistency execution environment to a relaxed memory context. Specifically, it considers the PSO (Partial Store Order) memory model, which corresponds to the use of a store buffer for each shared variable and each process. We also will consider, as an intermediate step, the TSO (Total Store Order) memory model, which corresponds to the use of one store buffer per process. The proposed approach extends a previously developed verification tool that uses finite automata to symbolically represent the possible contents of the store buffers. Its starting point is a program that is correct for the usual Sequential Consistency (SC) memory model, but that might be incorrect under PSO with respect to safety properties. This program is then first analyzed and corrected for the TSO memory model, and then this TSO-safe program is analyzed and corrected under PSO, producing a PSO-safe program. To obtain a TSO-safe program, only store-load fences (TSO only allows store-load relaxations) are introduced into the program. Finaly, to produce a PSO-safe program, only store-store fences (PSO additionally allows store-store relaxations) are introduced. An advantage of our technique is that the underlying symbolic verification tool makes a full exploration of program behaviors possible even for cyclic programs, which makes our approach broadly applicable. The method has been tested with an experimental implementation and can effectively handle a series of classical examples. [less ▲]

Detailed reference viewed: 90 (15 ULg)
Full Text
See detailVerifying Programs on Relaxed Memory Models with a Focus on x86-TSO
Linden, Alexander ULg

Conference (2011, September 28)

Model-checking tools classicaly verify concurrent programs under the traditional Sequential Consistency (SC) memory model, in which all accesses to the shared memory are immediately visible globally ... [more ▼]

Model-checking tools classicaly verify concurrent programs under the traditional Sequential Consistency (SC) memory model, in which all accesses to the shared memory are immediately visible globally. However, modern multiprocessor architectures implement relaxed memory models, such as Total Store Order (TSO) (or its extension with locks x86-TSO), which allow many more possible executions and thus can introduce errors that were not present in SC. Of course, one can force a program executed in the context of TSO to behave exactly as in SC by adding synchronization operations after every memory access. But this totally defeats the performance advantage that is precisely the motivation for implementing relaxed memory models, rather than SC. Thus, when moving a program to an architecture implementing a relaxed memory model (which includes most current multi-core processors), it is essential to have tools to help the programmer check if correctness (i.e. a safety property) is preserved and, if not, to minimally introduce the necessary synchronization operations. The proposed verification approach uses an operational store-buffer based semantics of the chosen relaxed memory model and proceeds by using finite automata for symbolically representing the possible contents of the buffers. Store, load, commit and other synchronization operations then correspond to operations on these finite automata. The advantage of this approach is that it operates on (potentially infinite) sets of buffer contents, rather than on individual buffer configurations, and that it is compatible with partial order reduction techniques. This provides a way to tame the explosion of the number of possible buffer configurations, while preserving the full generality of the analysis. It is thus possible to check even designs that exploit the relaxed memory model in unusual ways, and that may contain cycles. We have also proposed a memory fence insertion algorithm that finds how to preserve the correctness of a program when it is moved from SC to TSO. Its starting point is a program that is correct for the usual sequential consistency memory model (with respect to a given safety property), but that might be incorrect under x86-TSO. This program is then analyzed for this relaxed memory model and when errors are found (a broken safety property), memory fences are inserted in order to avoid these errors. The approach proceeds iteratively and heuristically, inserting memory fences until correctness is obtained, which is guaranteed to happen. In future work, we will investigate how to adapt our techniques to other common memory models, such as Partial Store Order (PSO), as well as how to optimally use the partial order reduction techniques. [less ▲]

Detailed reference viewed: 118 (28 ULg)
Full Text
Peer Reviewed
See detailA Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems
Linden, Alexander ULg; Wolper, Pierre ULg

in Lecture Notes in Computer Science (2011, July)

This paper addresses the problem of verifying and correcting programs when they are moved from a sequential consistency execution environment to a relaxed memory context. Specifically, it considers the ... [more ▼]

This paper addresses the problem of verifying and correcting programs when they are moved from a sequential consistency execution environment to a relaxed memory context. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds to the use of store buffers, and its extension x86-TSO, which in addition allows synchronization and lock operations. The proposed approach uses a previously developed verification tool that uses finite automata to symbolically represent the possible contents of the store buffers. Its starting point is a program that is correct for the usual sequential consistency memory model, but that might be incorrect under x86-TSO. This program is then analyzed for this relaxed memory model and when errors are found (with respect to safety properties), memory fences are inserted in order to avoid these errors. The approach proceeds iteratively and heuristically, inserting memory fences until correctness is obtained, which is guaranteed to happen. An advantage of our technique is that the underlying symbolic verification tool makes a full exploration possible even for cyclic programs, which makes our approach broadly applicable. The method has been tested with an experimental implementation and can effectively handle a series of classical examples. [less ▲]

Detailed reference viewed: 155 (52 ULg)
Full Text
Peer Reviewed
See detailAn Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
Linden, Alexander ULg; Wolper, Pierre ULg

in Lecture Notes in Computer Science (2010, September)

This paper addresses the problem of verifying programs for the relaxed memory models implemented in modern processors. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds ... [more ▼]

This paper addresses the problem of verifying programs for the relaxed memory models implemented in modern processors. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds to the use of store buffers. The proposed approach proceeds by using finite automata to symbolically represent the possible contents of the store buffers. Store, load and commit operations then correspond to operations on these finite automata. The advantage of this approach is that it operates on (potentially infinite) sets of buffer contents, rather than on individual buffer configurations. This provides a way to tame the explosion of the number of possible buffer configurations, while preserving the full generality of the analysis. It is thus possible to check even designs that exploit the relaxed memory model in unusual ways. An experimental implementation has been used to validate the feasibility of the approach. [less ▲]

Detailed reference viewed: 225 (80 ULg)