Abstract:
A system and method capable of finding relaxed memory-model vulnerabilities in a computer program caused by running on a machine having a relaxed memory model. A relaxed memory model vulnerability in a computer program includes the presence of program executions that are not sequentially consistent. In one embodiment, non-sequentially consistent executions are detected by exploring sequentially consistent executions.

Description:
BACKGROUND 
       [0001]    Developers of performance-critical multi-threaded software often try to avoid the overhead of traditional locking. Traditional techniques for doing so include making direct use of hardware primitives for atomic operations (such as interlocked exchange, or compare and swap) or employing regular loads and stores for the purpose of synchronization. Unfortunately, such “low-lock” programs are notoriously difficult to implement systems with a relaxed memory consistency model. Subtle bugs can arise in these programs due to memory operation reordering caused by the relaxed memory model of the underlying hardware. These errors are hard to find and debug as they most often show up only in specific thread interleavings and in particular hardware configurations. 
         [0002]    Low-lock code is used heavily both in low-level libraries and in critical paths of a system. Because these parts of the system are crucial to the reliability of the entire system, it is important to develop verification techniques. However, the high degree of non-determinism in relaxed memory consistency models challenges standard verification techniques. 
         [0003]    Previous attempts to programmatically find relaxed memory model bugs have attempted to solve the problem by modeling the potential executions of a program executing on a computer having a relaxed memory model. Due to the afore-mentioned non-determinism, these attempts do not scale. 
         [0004]    The memory consistency model is one of the major attributes of shared memory multiprocessor systems. It establishes a contract between the hardware and software regarding the behavior of accesses to shared memory. Its implication is not only limited to functionality; it also impacts performance and programmability of the system as well as portability on the software side and compatibility on the hardware side. 
       SUMMARY 
       [0005]    This document describes techniques capable of finding bugs in a computer program caused by running the computer program on a machine having a relaxed memory model. In one embodiment, an analysis algorithm, embodied in a “relaxed memory model error detection module” or “detection module”, executes the program under test in many ways, through many different code paths. Each distinct code path is known as an “execution” of the program under dest. The analysis algorithm may detect the existence of non-sequentially consistent executions of the program under test while analyzing only sequentially consistent executions of the program under test. In one embodiment, individual executions of the program under test, such as executions obtained by running the program in a testing environment, are analyzed by the detection module. In another embodiment, all executions of the program are systematically enumerated and analyzed by the detection module. In one embodiment, the detection module is run simultaneously with the program under test; in another embodiment, a trace file is first generated from the program under test and the detection module analyzes that trace file offline. 
         [0006]    In yet another embodiment, the detection module receives a memory trace comprising a plurality of memory access events each representing the execution of a memory access instruction issued by the program under test on a computer having a sequentially consistent memory model. The detection module determines whether the memory access instructions could, when executed on a computer having a relaxed memory model, be executed in an order in which they could not have been executed on the sequentially consistent computer. The result of the determination is an indication whether or not the memory access instructions, and thus the test computer program they were derived from, are relaxed memory model safe. 
         [0007]    This Summary is provided to introduce a selection of concepts in a simplified form that are further described below in the Detailed Description. This Summary is not intended to identify key features or essential features of the claimed subject matter, nor is it intended to be used to limit the scope of the claimed subject matter. 
     
    
     
       BRIEF DESCRIPTION OF THE CONTENTS 
         [0008]    The detailed description is described with reference to accompanying figures. In the figures, the left-most digit(s) of a reference number identifies the figure in which the reference number first appears. The use of the same reference numbers in different figures indicates similar or identical items. 
           [0009]      FIG. 1  depicts an illustrative relaxed memory model error detection system, showing two alternative embodiments. As illustrated, both embodiments include a detection module. 
           [0010]      FIG. 2A  depicts illustrative components of a sequentially consistent memory model and a relaxed memory model. 
           [0011]      FIG. 2B  depicts a conceptual implementation of store buffers. 
           [0012]      FIG. 3  depicts an illustrative execution of two threads, as well as the “happens before” relationships used to identify borderline executions. 
           [0013]      FIG. 4  depicts illustrative components of a relaxed memory error detection module. 
           [0014]      FIG. 5  depicts an illustrative process for deriving a memory trace from an execution stream, and analyzing the memory access instructions to determine if they could be executed in a different order. 
           [0015]      FIG. 6  depicts an illustrative process for determining if a memory trace representing memory access instructions exhibits relaxed memory model bugs. 
           [0016]      FIG. 7  depicts an illustrative process for determining if a memory trace representative of all possible memory traces of a test program exhibit relaxed memory model bugs. 
           [0017]      FIG. 8  depicts an illustrative process for determining if a memory trace representing memory access instructions exhibits relaxed memory model bugs. 
       
    
    
     DETAILED DESCRIPTION 
       [0018]    The following discussion targets techniques capable of finding bugs in a computer program caused by running on a machine having a relaxed memory model. 
         [0019]    Multiprocessor computers are complicated systems, and writing software to take advantage of the processing power of a multiprocessor computer has proven challenging. One reason is the existence of a class of bugs that arises in multiprocessor computing systems having relaxed memory access models. This class of bugs includes undefined behaviors of a computer program that are only possible when the computer program is executed on a computer having a relaxed memory access model. One example of a relaxed memory model susceptible to this class of bugs is the Total Store Order, or TSO, memory model, as discussed below. Other relaxed memory models include 390, Relaxed Memory Order (RMO), Power PC (PPC), and Intel Architecture 32 (IA-32). While the techniques discussed herein consider a TSO memory model, the same techniques apply equally to these and other relaxed memory models. 
         [0020]    More conservative memory models, meanwhile, may not be as susceptible to this class of bugs. One example of a conservative memory model is a sequentially consistent memory model, as discussed below. The class of bugs detected is typically encountered when a program written for a conservative memory model is executed on a computer having a relaxed memory model. 
         [0021]    A memory access model, or memory consistency model, defines the behavior of a shared system memory. This model also defines how that shared system memory is accessed by processors in the system. For instance, a sequentially consistent memory model on a multiprocessor system limits access to the computer&#39;s shared memory such that only one processor at a time may read from or write to the shared system memory. By limiting access to one processor a time, and by ensuring that all memory access operations are completed before another processor is allowed to access the shared memory, the sequentially consistent memory model ensures a high level of memory integrity. For example, on a computer with a sequentially consistent memory model, the system prevents a processor from accessing a stale memory value by ensuring that all store instructions are committed to the shared system memory before a second processor is allowed to load a value from that memory address. 
         [0022]    However, by limiting access to the shared system memory, a sequentially consistent memory model creates a performance bottleneck as processors will frequently idle while waiting for the processor currently accessing the shared system memory to finish. In order to allow parallel, concurrent access to the shared system memory, relaxed memory models have been designed to allow some balance of memory system integrity and overall system performance. 
         [0023]    A computer having a TSO memory model typically includes more than one processor, and each processor includes a store buffer with store-load forwarding. Store-load forwarding enables a processor to store a value to its local store buffer (also called a cache) without committing that value to the shared system memory. By not committing the new value to the shared system memory, all of the other processors will access the stale value residing in the shared system memory until the new value is committed from the cache to the system memory. Additionally, a TSO memory model provides no guarantee as to when the new value stored in the first processor&#39;s store buffer will be committed to the shared system memory. As a consequence, programmers who do not properly consider this store buffer indeterminism will often write code that includes undefined or unexpected behaviors when executed on a TSO memory model. Because this undefined program behavior is almost always a bug, relaxed memory model bugs are defined as program behaviors that are possible when executed on a relaxed memory model but not possible when executed on a sequentially consistent memory model. 
         [0024]    In other embodiments, computer systems comprising relaxed memory models may include hardware devices that reorder memory accesses, such as out-of-order or multiple-issue instruction pipelines, memory access buffers, data caches with asynchronous write-through, and/or victim buffers. In other embodiments, computer systems comprising relaxed memory models may include software components that reorder memory accesses, such as compilers performing optimizing program transformations that move, introduce, or eliminate memory accesses or synchronization instructions. 
         [0025]    In one embodiment, relaxed memory model bugs are found in a test program by analyzing all possible program executions on a sequentially consistent memory model, and determining whether additional executions are possible on a relaxed memory model. A program execution (or interleaving) comprises a sequence in which a plurality of instructions of the test computer program are executed. For example, the first execution of an application typically begins at the beginning of the entry point function. If the application can be passed command line arguments, different executions are likely to exist within the entry point function. For instance, when a command line argument is passed to the application, an execution parsing and responding to the command line arguments will be executed. When the application is run without a command line argument, a different execution may be taken. Only by searching for bugs in all possible locations can all relaxed memory model bugs be found in the test application. 
         [0026]    The number of potential executions contained in a given application can vary widely. In some cases, applications will be completely deterministic, and so there is only one execution for that test program. In other cases, applications may contain branching instructions or exception handling functions, but may or may not be executed. In still other cases, a test program may contain multiple threads, increasing the number of ways in which a series of instructions can be executed, due to the indeterminacy of the thread scheduler. Applications that respond to user input, network traffic, or any other random or pseudo-random input also may include a large number of possible executions. Importantly, the number of possible executions additionally depends on aspects of the computer on which the application is executing. For instance, on a computer having a sequentially consistent memory model, there may be fewer possible executions of the test program then the same program might have when executed on a computer having a relaxed memory model. By identifying executions that are only possible when executing on a computer having a relaxed memory model, relaxed memory model bugs can be identified. Minimal executions, which are executions that are only possible when executed on a computer having a relaxed memory model, are defined as borderline executions. 
         [0027]    Relaxed memory model bugs are often introduced because the developer of the application assumed the application would always execute on a computer having a sequentially consistent memory model. Consequently, whenever borderline executions are possible, the additional executions may likely comprise bugs, because the additional executions are undefined or unexpected. Only when a computer having a relaxed memory model and a computer having a sequentially consistent memory model generate identical executions is the test program relaxed memory model safe. 
         [0028]      FIG. 1  depicts an illustrative relaxed memory model error detection system  100 . In one embodiment, a relaxed memory model error detection module  102  receives a memory trace  104  that was generated by a stateless model checker  106 . The relaxed memory model error detection module  102  may be a software module running on a central processing unit or a hardware device similarly programmed (or a combination thereof). The relaxed memory model error detection module  102  may comprise a standalone computer application, or alternatively may be a module included or embedded in a generalized error detection application. 
         [0029]    The memory trace  104  includes a series of memory access events. The memory access events comprise memory loads, memory stores, and interlocked memory operations. Each memory access event corresponds to a memory access instruction that was executed by a test program. The memory trace  104  may be passed to the detection module  102  on the fly, such as in the form of procedure calls, a message stream, or other forms of intra- or inter-process communication. Alternatively, the memory trace  104  may be passed to the detection module offline, such as by storing it to a trace file or another form of permanent or transient storage, from where the detection module  102  may read the memory trace at a later time. 
         [0030]    The stateless model checker  106  receives an executable program  112  as input. The stateless model checker  106  processes the executable program  112 , enumerating every possible execution on a sequentially consistent memory model. Alternatively, the stateless model checker  106  may enumerate a representative subset of every execution, wherein the representative subset of executions are sufficient to enable the relaxed memory model error detection module  102  to detect any borderline execution in the executable program  112 . 
         [0031]    The relaxed memory model error detection module  102  alternatively or additionally receives a memory trace  108 . The memory trace  108  may similarly comprise memory access events, the memory access events comprising memory loads, memory stores, and interlocked memory operations. Again, the memory trace  108  may be passed to the detection module  102  on the fly, such as in the form of procedure calls, a message stream, or other forms of intra- or inter-process communication. Alternatively, the memory trace  108  may be passed to the detection module  102  offline, such as by storing it to a trace file or another form of permanent or transient storage, from where the detection module  102  reads the memory trace  108 . 
         [0032]    An instrumentation and logging module  110  generates the memory trace. The instrumentation and logging module  110  receives an executable program  114  as input, and instruments the executable program  114  such that when executed, memory instructions executed by the instrumented program  114  are trapped. Memory access events corresponding to the trapped memory access instructions are then created and added to the memory trace  108 . In this way, instrumentation and logging module  110  enables tracing the memory access instructions that are actually executed by the executable program  114 . Therefore it is possible that the executable program  114  contains undetected borderline executions that were not detected because the borderline executions were not actually executed. While merely tracing actual executions of an application may miss some borderline executions, it may be the only practical way to analyze a very large test program containing a very large number of executions to enumerate. An example of an application that is so large it may not efficiently enumerate all executions is Microsoft Word® or Microsoft Internet Explorer®. 
         [0033]      FIG. 2A  depicts illustrative components  200  of a sequentially consistent memory model and a relaxed memory model. Many implementations are contemplated, including software, hardware, and a combination thereof. A sequentially consistent memory model  202  may include multiple processors. While the sequentially consistent memory model is illustrated with three processors, any number of one or more processors is similarly contemplated. A processor  206 , a processor  208 , a the processor  210  are electrically connected to a shared memory  214 . However, in the sequentially consistent memory model only one processor is granted access to the shared memory  214  at any one time. 
         [0034]    As illustrated in  FIG. 2B , a relaxed memory model  204  enables a processor  214  and a processor  218  to simultaneously access a shared memory  222 . The processor  214  may comprise a store-load a buffer  220 . Alternatively, the processor  214  may be electrically connected to the store-load buffer  220 . Similarly, the processor  218  may comprise a store-load buffer  222 , or alternatively the processor  218  may be electrically connected to the store-load buffer  222 . As will be explained below, the relaxed memory model  204  may execute the same code as the sequentially consistent memory model  202 , yet obtain different results. 
         [0035]      FIG. 2C  illustrates the execution of a simple set of memory access instructions that may achieve different results based on which memory model they are executed on. Both a sequentially consistent execution  224  and a relaxed execution  226  operate on variables and A and B, with both initialized to “0” in the current example. The sequentially consistent execution  224  is about to execute instructions “Store A, 1” and “Store B, 1” simultaneously on processors  206  and  208 , respectively. The second set of instructions, “Load B” and “Load A”, look as if they will be executed immediately afterward. When executed by the sequentially consistent execution  224 , there is no one set of resulting values for A &amp; B: A may hold the value “0” while B holds “1”, B may hold “1” while A holds “0”, or both A and B may hold “1 ”. However, it is not possible for both A &amp; B to hold the value “0”. 
         [0036]    There are two initial possibilities to consider when executing these instructions on a sequentially consistent machine: either the processor  206  is granted access to the shared memory  214  first, or the processor  208  is granted access to the shared memory  214  first. If the processor at  206  is granted access to the shared memory  214  first, a value of 1 will be stored at location A. Because of the nature of the sequentially consistent memory model  202 , the processor  208  will not be allowed to execute the “Store B, 1” execution until the processor  206  no longer has exclusive access to the shared memory  214 . Alternatively, the processor  208  may be granted first access to the shared memory  214  first, in which case “Store B,1” will be executed first, and the processor  206  have to wait before executing “Store A,1”. 
         [0037]    Once the initial processor (either the processor  206  executing “Store A,1” or the processor  208  executing “Store B,1”) has executed its first instruction, there are two additional possibilities. Either the initial processor will maintain exclusive access to the shared memory  214 , and execute the second instruction before the other processor has executed its first instruction, or the initial processor will relinquish exclusive access to the shared memory  214  after executing its first instruction, and allow the other processor to execute its first instruction. 
         [0038]    First consider the scenario when the first processor to execute completes execution before the other processor executes any of its instructions. If, for example, the processor  206  begins by executing “Store A,1”, and does not relinquish the shared memory  214 , the processor  206  will then execute “Load B”, all before the processor  208  executes “Store B,1”. Therefore, the value of “B” loaded from the shared memory  214  will be “0”. Once the processor  208  is allowed to begin execution, “Store B,1” assigns 1 to “B” and “Load A” loads the value “1” into A. The sequence of instructions is as follows:
       1) “Store A,1”   2) “Load B”   3) “Store B,1”   4) “Load A”.       
 
         [0043]    Therefore, this scenario yields a result of A=1 and B=0. The same sequence, but with the processor  208  executing first, will result in B=1 and A=0. 
         [0044]    On the other hand, when one of the processors executes its first instruction, and then relinquishes access to the shared memory  214 , the other processor may then execute its first instruction. In this scenario both variables will be assigned a value “1” before any of the “Load” instructions have been executed, resulting in both variables having the value “1”. 
         [0045]    While it is possible when executing these instructions on a sequentially consistent memory model to achieve any the three results listed above, there is no scenario where executing these memory access instructions results in both variables having the value “0”. 
         [0046]    However, as shown by the relaxed execution  226 , executing the same memory access instructions on the relaxed memory model  204  allows this fourth possibility. This additional execution—a borderline execution, is possible due to the nature of the relaxed memory model  204 . In this scenario, a processor  214  and a processor  218  both simultaneously execute their respective store instructions. Because these processors are executing in the relaxed memory model  204 , they are both allowed to access the shared memory  222  concurrently. Additionally, the values stored in variables “A” and “B” may not be committed to the shared memory  222 . Instead, the values stored in variables “A” and “B” may be cached in the local store-load buffers  220  and/or  222 . When both processors concurrently execute the “Load B” and “Load A” instructions, both processors may read the stale value of “0” out of the shared memory  222 , because the new values may have not yet been committed to the shared memory  222 . This fourth execution is an example of a borderline execution because it only occurs when executed on a computer having a relaxed memory model. 
         [0047]      FIG. 3  depicts an illustrative execution of two threads, including the “happens before” relationship and the relaxed “happens before” relationship used in one embodiment to identify borderline executions. A “happens before” (hb) relationship exists between two memory access events executed by a sequentially consistent memory model when it can be known that a first event will be executed earlier in time than a second event. Similarly, a “relaxed happens before” (rhb) relationship exists between the first and second memory access events on a relaxed memory model when it can be known that the first event will always be executed before the second event. The nature of the “happens before” and relaxed “happens before” relationships are such that the existence of either relationship between two memory access events implies the second event could never be executed before the first event. Inversely, if there is no “happens before” or relaxed “happens before” relationship between two memory access events, it is possible for the second event to be executed before the first event. 
         [0048]    Typically, the second event can be executed before the first event on relaxed memory model when the first event is a “Store”. This is true because the “Store” instruction only guarantees that the stored value exists in the buffer local to the processor that executed the instruction. There is no guarantee that the stored value has been committed to the shared system memory  224 , and so it is possible that the second event will complete execution before the first event completes execution. In one embodiment, the relaxed memory model error detection module  102  may detect a borderline execution by locating two events for which a “happens before” relationship exists, but a “relaxed happens before” relationship does not exist, indicating that the memory access instructions are not relaxed memory model safe. 
         [0049]    In one preferred embodiment, vector clocks are used to determine whether a “happens before”, in the case of a sequentially consistent memory model, or a “relaxed happens before”, in the case of a relaxed memory model, relationship exists. In other embodiments, the relaxed memory model error detection module  102  may construct a graph representing “happens before” and “relaxed happens before”. 
         [0050]      FIG. 3A  graphically illustrates “happens before” relationships that exist between the listed memory access events.  FIG. 3B  graphically illustrates “relaxed happens before” relationships that exist between the listed memory access events. 
         [0051]    In one embodiment, a memory access event includes a memory access type identifier, the memory address accessed by the memory access event (represented here by variables A. and B), and a coherence index. The coherence index indicates which Load or Store instruction, in the sequence of Load and Store instructions, the current memory access event represents. For example, the memory access event “(1,0) Store B, 1” illustrates a “Store” event, wherein the value is stored in memory address “B”, and the coherence index is “1” (because this is the first store instruction at address B). 
         [0052]    A sequentially consistent memory module  302  includes a thread  306  and a thread  308 , each thread executing on different processors (not shown). A “happens before” (hb) relationship exists between two memory access events when it can be known that the first event will always happen before the subsequent, second event. For example, by the sequential nature of execution on the sequentially consistent memory model  302 , “(1,0) Store B,1” is known to complete before “(2,0) Store A, 1” will be executed. Therefore, a “happens before” relationship exists between “(1,0) Store B,1” and “(2,0) Store A,1”. 
         [0053]    Similarly, a “happens before” relationship exists between “(2,0) Store A,1” and “(2,1) Load A,1”. In this case, the Store event begins execution before the Load event, and the Load event loads the value stored by the Store event, so due to the nature of the sequentially consistent memory model  302 , the Store event is guaranteed to complete execution before the Load event executes. 
         [0054]    Finally, “(2,1) Load A,1” has a “happens before” relationship with “(2,2) Load B,1” for the same reason “(1,0) Store B,1” has a “happens before” relationship with “(2,0) Store A, 1”. Importantly, due to the transitive nature of the “happens before” relationship, in one embodiment it can be known that a “happens before” relationship exists between “(1,0) Store B,1” and “(2,2) Load B,1”. 
         [0055]    A relaxed memory model  304  includes a thread  310  and a thread  312 , each thread executing on a different processor (not shown). A “relaxed happens before” (rhb) relationship exists between two memory access events when it can be known that one event will always happen before the subsequent event. In this example, there is no relaxed “happens before” relationship between “Store A,1” and “Load B,0”, due to the store buffer associated with the processor executing the thread  310 . 
         [0056]    Similarly, “Store B,1” does not have a “relaxed happens before” relationship with “Load A,?”. Due to the indeterminate nature of when a Store event will be committed to the shared system memory, it is not possible to know whether A will be loaded with the value 1, or 0. In order for there to exist a “happens before” relationship between “Store A,1” and “Load A,?”, intervening memory access events must also have a “relaxed happens before” relationship, which is not the case in the relaxed memory model  304 . It is possible for the “Store A,1” instruction to have stored the value “1” in the thread  310 &#39;s store buffer without updating the shared system memory. In this case, the “Load A,?” instruction would load a “0”. However, if the value “1” was committed before “Load A,?” is execute, the value loaded in “A” would be “1”. 
         [0057]    The execution exhibited in  FIG. 3B  is another example of a borderline execution: if the same code were executed on a sequentially consistent memory model, the final “Load” instruction would always load “1”. 
         [0058]      FIG. 3B  does exhibit a relaxed “happens before” relationship between “Load B,0” and “Store B,1”, because the Load is executed before the store, and due to the nature of a Load (which never has to wait for a store buffer to commit), “Load B,0” will always execute before “Store B,1”. 
         [0059]    In one embodiment, the existence of a “relaxed happens before” relationship can be determined in part by the use of vector clocks. Vector clocks are used in multiprocessor systems to identify causalities in concurrent executions of programs. In such a system, each processor includes an actual clock in addition to a pseudo-clock that shadows the remaining real clocks in the system. Each actual clock may be a timer, or alternatively the clock may be a sequence number that increments every time the clock is accessed. When a message is sent from a first processor to a second processor, the first processor creates a timestamp from the current state of its actual clock and its pseudo-clocks. Upon receipt at the second processor, the second processor will update its pseudo-clocks with values stored in the event&#39;s timestamp, merging the highest values from the second processor&#39;s existing pseudo-Clocks with the values stored in the event&#39;s timestamp. 
         [0060]    Given two vector clock timestamps, it is possible to know which timestamp was created first in time by comparing the values of the timestamps to each other. If all of the values of a first timestamp are less than or equal to the respective values of a second timestamp, the first timestamp is known to have been created first. 
         [0061]      FIG. 4  depicts illustrative components of a relaxed memory error detection module. The relaxed memory error detection module  102  receives a memory trace comprising memory access events  402 , such as loads, stores, and interlocked memory operations. The interlocked memory operations may represent any kind of atomic operation, such as a memory fence, locks, semaphores, mutexes, critical sections, and spin locks, etc. Each of these operations is translated by the stateless model checker  106  into a generic Interlocked memory operation. Each execution contained within the memory trace is analyzed twice, once by a sequentially consistent memory model analyzer  404 , and once by a relaxed memory model analyzer  406 . In one embodiment, the sequentially consistent memory model analyzer  404  utilizes a traditional vector clock algorithm to determine the existence of “happens before” relationships. In one embodiment, the relaxed memory model analyzer  406  utilizes the novel vector clock algorithm listed below to determine the existence of relaxed happen before relationships. 
         [0062]    The relaxed memory model analyzer  406  analyzes each memory access event e o  . . . e n  in an execution of some test program to determine the existence of “relaxed happens before” relationships. The relaxed memory model analyzer  406  utilizes the novel vector clock algorithm described below to calculate timestamps t o  . . . t n , such that a “relaxed happens before” relationship exists between events e i  and e j  if and only if (i≦j) and (t i [k]≦t j [k]) for all k in {1, . . . , 2N}. 
         [0063]    Included below is one example of pseudo-code for calculating the vector clocks used in the above algorithm to determine whether or not a “relaxed happens before” relationship exists: 
         [0000]    
       
         
               
               
               
             
               
               
             
           
               
                   
               
             
             
               
                 1 
                 type 
                 timestamp: array[2*N] of No; 
               
               
                 2 
                 var lc: 
                 array[Proc] of timestamp; 
               
               
                 3 
                 sc: 
                 array[Proc] of timestamp; 
               
               
                 4 
                 mc1: 
                 array[Proc][Adr] of timestamp; 
               
               
                 5 
                 mc2: 
                 array[Adr] of timestamp; 
               
             
          
           
               
                 6 
                 initially lc[*][*] = sc[*][*] = mc1[*][*][*] = mc2[*][*] = 0; 
               
               
                 7 
                 function merge(ts1, ... tsn : timestamp) returns timestamp { 
               
               
                 8 
                  return (maxi(tsi[1]), ... , maxi(tsi[N*2])); 
               
               
                 9 
                 } 
               
               
                 10 
                  function process_event(e : Evt) returns timestamp { 
               
               
                 11 
                  match e with 
               
               
                 12 
                   ld(p,i,a,c) -&gt; 
               
               
                 13 
                    ts := merge(lc[p], mc1[p][a]); 
               
               
                 14 
                    ts[2*p] := ts[2*p] + 1; // advance load count for p 
               
               
                 15 
                    lc[p] := merge(lc[p], ts); 
               
               
                 16 
                    mc2[a] := merge(mc2[a], ts); 
               
               
                 17 
                   st(p,i,a,c) -&gt; 
               
               
                 18 
                    ts := merge(sc[p], lc[p], mc2[a]); 
               
               
                 19 
                    ts[2*p+1] := ts[2*p+1] + 1; // advance store count for p 
               
               
                 20 
                    forall q 6= p do 
               
               
                 21 
                    mc1[q][a] := merge(mc1[q][a], ts); 
               
               
                 22 
                    mc2[a] := merge(mc2[a], ts); 
               
               
                 23 
                    sc[p] := merge(sc[p], ts); 
               
               
                 24 
                   il(p,i,a,c) -&gt; 
               
               
                 25 
                    ts := merge(sc[p], lc[p], mc2[a]); 
               
               
                 26 
                    ts[2*p] := ts[2*p] + 1; // advance load count for p 
               
               
                 27 
                    ts[2*p+1] := ts[2*p+1] + 1; // advance store count for p 
               
               
                 28 
                    forall q 2 Proc do 
               
               
                 29 
                    mc1[q][a] := merge(mc1[q][a], ts); 
               
               
                 30 
                    mc2[a] := merge(mc2[a], ts); 
               
               
                 31 
                    lc[p] := merge(lc[p], ts); 
               
               
                 32 
                    sc[p] := merge(sc[p], ts); 
               
               
                 33 
                   return ts; 
               
               
                 34 
                 } 
               
               
                   
               
             
          
         
       
     
         [0064]    Finally, in one embodiment a relaxed memory model safety algorithm  408  analyzes the “happens before” and “relaxed happens before” relationships calculated above to determine if the memory access events  402  are relaxed memory model safe. The relaxed memory model safety algorithm  408  searches for borderline executions, which comprise two events for which there exists a “happens before” relationship, but not a “relaxed happens before” relationship. The existence of a borderline execution indicates that a memory access instruction can be executed in a different order on a computer having a relaxed memory model, which means the memory access events  402  are not relaxed memory model safe. Additionally, the relaxed memory model safety algorithm  408  ensures that for each event in an execution, all of the previously executed events in that execution have a “happens before” relationship with that event. Included below is the pseudo-code for ensuring relaxed memory model safety: 
         [0000]    
       
         
               
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 1 
                 function is_store_buffer_safe(e1e2 . . . en) returns boolean { 
               
               
                   
                 2 
                  var k,p,a,c : N; var E : T ; 
               
               
                   
                 3 
                  E := Ø; 
               
               
                   
                 4 
                  for (k := 1; k &lt;= n; k++) { 
               
               
                   
                 5 
                   if (o(ek) = ld) { 
               
               
                   
                 6 
                    p := p(ek); a := a(ek); c := c(ek); 
               
               
                   
                 7 
                    while (c &gt; 0) { 
               
               
                   
                 8 
                     if (p = i(write(E,a,c))) 
               
               
                   
                 9 
                      break; 
               
               
                   
                 10 
                      if (write(E,a,c) !_rhb lastR(E,p)) 
               
               
                   
                 11 
                       break; 
               
               
                   
                 12 
                      if (write(E,a,c) !_hb last(E,p)) 
               
               
                   
                 13 
                       return false; 
               
               
                   
                 14 
                      c := c − 1; 
               
               
                   
                 15 
                    } 
               
               
                   
                 16 
                   } 
               
               
                   
                 17 
                   E := E U ek; 
               
               
                   
                 18 
                  } 
               
               
                   
                 19 
                  return true; 
               
               
                   
                 20 
                 } 
               
               
                   
                   
               
             
          
         
       
     
         [0065]      FIG. 5  depicts an illustrative environment  500  for deriving a memory trace from an execution stream, and analyzing the memory access instructions to determine if they could be executed in a different order. 
         [0066]    An instruction stream  502  is executed by the processor  202 . Additionally, an instruction stream  504  is executed by the processor  204 . The stateless model checker  106  extracts memory access instructions from the processors  202  and  204 , and generates the memory trace  104 . The memory trace  104  is analyzed by the relaxed memory model error detection module  102  to determine if there exist any borderline executions in the memory trace  104 . The relaxed memory model error detection module  102  determines if any borderline executions exist by analyzing each instruction to see if that instruction could have been executed before any of the previously executed instructions on a computer having a relaxed memory model. 
         [0067]      FIG. 6  depicts an illustrative process for determining if a memory trace representing memory access instructions exhibits relaxed memory model bugs. Operation  602  represents receiving a memory trace generated from executing a test program on a sequentially consistent computer. Operation  604 , meanwhile, determines whether the memory access instructions represented by the memory trace could be executed in a different order on a relaxed memory model computer. Operation  606  outputs an indication that the memory access instructions represented by the memory trace are relaxed memory model safe when it is not possible for the memory access instructions to be executed in a different order. Operation  608  outputs an indication that the memory access instructions represented by the memory trace are not relaxed memory model safe when it is possible for the memory access instructions to be executed in a different order. 
         [0068]      FIG. 7  depicts an illustrative process for determining if a memory trace representative of all possible memory traces of a test program exhibit relaxed memory model bugs. Operation  702  represents receiving a plurality of memory traces generated by a stateless model checker. Operation  704 , meanwhile, determines whether any of the memory access instructions represented by the memory trace could be executed in a different order on a computer having a relaxed memory model. Operation  706  provides an indication whether or not the plurality of memory traces are relaxed memory model safe. 
         [0069]      FIG. 8  depicts an illustrative process for determining if a memory trace representing memory access instructions exhibits relaxed memory model bugs. Operation  802  receives a memory trace comprising memory access instructions generated from a sequentially consistent memory model. Operation  804 , meanwhile, determines if the memory access instructions could be executed in a different order when executed on a computer having a relaxed memory model. Operation  806  determines whether the memory access instructions could be executed in a different order when executed on a computer having a relaxed memory model by comparing each memory access instruction with previously executed memory access instructions. Operation  808  determines whether a memory access instruction could be executed before one of the previously executed memory access instructions due to store-load forwarding. Operation  810  outputs an indication of whether or not the memory access instructions are relaxed memory model safe. 
         [0070]    Conclusion 
         [0071]    Although the subject matter has been described in language specific to structural features and/or methodological acts, it is to be understood that the subject matter defined in the appended claims is not necessarily limited to the specific features or acts described above. Rather, the specific features and acts described above are disclosed as example forms of implementing the claims.