# Patent

## Title
Accelerating model checking via synchrony

## Abstract

A system and method for program verification by model checking in concurrent programs includes modeling each of a plurality of program threads as a circuit model, and generating a full circuit for an entire program by combining the circuit models including constraints which enforce synchronous execution of the program threads. The program is verified using the synchronous execution to reduce an amount of memory needed to verify the program and a number of steps taken to uncover an error.

## Background
RELATED APPLICATION INFORMATION
This application claims priority to provisional application Ser. No. 60/916,339 filed on May 7, 2007 incorporated herein by reference.


BACKGROUND
1. Technical Field
The present invention relates to software verification and debugging and more particularly to systems and methods for accelerating model checking by providing synchronous execution constraints.
2. Description of the Related Art
The development of effective techniques for debugging multi-threaded software is widely recognized to be a problem of fundamental practical importance. It is, however, also an extremely challenging one. A key reason for this is that subtle interactions between threads makes multi-threaded software behaviorally complex and hard to analyze, thus necessitating the use of formal methodologies for the analysis. It is not surprising then that the use of model checking—both symbolic and explicit state—for the verification of concurrent software has, for some time, been an active area of research.
Explicit state model checkers, such as VerisoftTM rely on exploring an enumeration of the states and transitions of the concurrent program at hand. Additional techniques such as state hashing for compaction of state representations, and partial order methods are typically used to avoid exploring all interleavings of transitions of the constituent threads. Symbolic model checkers, on the other hand, avoid an explicit enumeration of the state space by using symbolic representations of sets of states and transitions.
One of the first successful approaches in this regard was the use of BDDs to succinctly represent large state spaces for the purpose of model checking. More recently, SAT-based techniques have become popular both for finding bugs using SAT-based Bounded Model Checking (BMC) and for generating proofs via SAT-based Unbounded Model Checking (UMC).
SAT-based techniques strongly rely on search heuristics in order to prune state spaces. A lot of these heuristics depend on leveraging structural information about the system at hand. As a result SAT-based BMC has been shown to be very effective for debugging hardware designs which have a lot of inherent organization that these heuristics exploit. Since software programs are much less structured than hardware circuits developing similar heuristics has proven to be a more difficult problem.
SUMMARY
A system and method for program verification by model checking in concurrent programs includes modeling each of a plurality of program threads as a circuit model, and generating a full circuit for an entire program by combining the circuit models including constraints which enforce synchronous execution of the program threads. The program is verified using the synchronous execution to reduce an amount of memory needed to verify the program and a number of steps taken to uncover an error.
A program verification system includes a plurality of circuit models wherein each circuit model represents a program thread in a concurrent program. A full circuit model represents the entire concurrent program, and the full circuit model is composed of a combination of the circuit models as bound by constraints which enforce synchronous execution of the program threads. A model checker is configured to verify the concurrent program using the synchronous execution to reduce an amount of memory needed to verify the concurrent program.
These and other features and advantages will become apparent from the following detailed description of illustrative embodiments thereof, which is to be read in connection with the accompanying drawings.



BRIEF DESCRIPTION OF DRAWINGS
The disclosure will provide details in the following description of preferred embodiments with reference to the following figures wherein:
FIG. 1 is a block/flow diagram of a system/method for program verification using model checking in accordance with one illustrative embodiment;
FIG. 2 is a block/flow diagram of a system/method for determining interesting states as temporal conflict pairs in accordance with one illustrative embodiment;
FIG. 3 is a diagram showing a simplified Büchi automaton for determining conflicts in accordance with one illustrative embodiment; and
FIG. 4 is a block/flow diagram of a system/method for incorporating/integrating synchronous execution and partial order reduction program verification using model checking in accordance with one illustrative embodiment.



DETAILED DESCRIPTION OF PREFERRED EMBODIMENTS
In typical real-life concurrent programs, most computation is done locally within threads with synchronization or shared variable accesses occurring infrequently. The present embodiments, exploit this parallelism inherent in threads, by leveraging synchronous execution to get drastic reductions in the depth of witness traces during model checking. In turn, this reduces the depth to which a program needs to be explored to reach an error. Note that each unroll step of a bounded model checking (BMC) run increases the size of the program under consideration thereby increasing memory usage. Since memory is the key bottleneck in the verification of large-scale programs, using synchronous execution provides advantages to (i) potentially use BMC on larger programs thus increasing scalability, and (ii) increase the depth to which programs can be explored. Furthermore, to ensure scalability, we also show how to effectively combine synchronous execution with symbolic model checking while at the same time leveraging partial order reduction and on-the-fly transactions.
To ensure that the temporal property being model checked is preserved during synchronous execution, we leverage a new notion of temporal conflicts. We show that temporal conflicts can also be used to improve partial order reduction techniques by permitting computation of smaller stubborn sets than the ones based on the notion of visible transitions.
Embodiments described herein may be entirely hardware, entirely software or including both hardware and software elements. In a preferred embodiment, the present invention is implemented in software, which includes but is not limited to firmware, resident software, microcode, etc.
Embodiments may include a computer program product accessible from a computer-usable or computer-readable medium providing program code for use by or in connection with a computer or any instruction execution system. A computer-usable or computer readable medium may include any apparatus that stores, communicates, propagates, or transports the program for use by or in connection with the instruction execution system, apparatus, or device. The medium can be magnetic, optical, electronic, electromagnetic, infrared, or semiconductor system (or apparatus or device) or a propagation medium. The medium may include a computer-readable medium such as a semiconductor or solid state memory, magnetic tape, a removable computer diskette, a random access memory (RAM), a read-only memory (ROM), a rigid magnetic disk and an optical disk, etc.
Referring now to the drawings in which like numerals represent the same or similar elements and initially to FIG. 1, a block/flow diagram shows a system/method 100 for improved model checking in accordance with one illustrative embodiment. In one embodiment, building circuits or SAT-based models 104 for threads 102 of concurrent multi-threaded programs is provided. Advantageously, existing powerful SAT-based techniques for hardware verification can be leveraged. This approach permits exploitation of the synergy that results from combining the ability of partial order techniques to reduce the state space of the system to be explored—with the power of symbolic model checking to explore large state spaces. An added advantage of modeling each thread 102 in a concurrent program as a circuit 104 is that for verification purposes, parallelism inherent in the threads can be exploited by executing these circuits synchronously.
In concurrent programs, shared variables are accessed in a very small number of functions. Most of the computation is done for threads locally and synchronization with other threads occurs infrequently. Thus, by executing the thread local code synchronously, we can get drastic reductions in the depths of witness traces for properties and, as a consequence, in the depth to which a program needs to be explored for detecting an error. This is important as each unroll step of a BMC run increases the size of the circuit under consideration thus increasing memory usage. Since memory is a key bottleneck in the verification of large designs, using synchronous execution, we can potentially use BMC on larger programs thus increasing the scalability as well as the depth to which they can be explored.
Synchrony can be used to accelerate the model checking of concurrent programs for LTL properties, for example. Executing a concurrent program synchronously changes its semantics and creates several challenges. First, we need to ensure that we do not miss any necessary interleavings induced by shared variable updates and synchronization primitives. Second, in switching from interleaving to synchronous semantics, the temporal property being model checked needs to be preserved. Finally, to address state explosion, we show how to integrate synchronous execution with partial order reduction, transactions and symbolic model checking.
The given concurrent program is translated into a circuit-based model or models 104. Assuming bounded data and bounded recursion, we obtain a finite model (104) for each individual thread 102 wherein each variable of the thread is represented in terms of a vector of binary-valued latches and a boolean next-state function for each latch. Then, using a scheduler, we compose the circuits for the individual threads into one single circuit 106 for the entire concurrent program. Verification is then carried out on this circuit in block 10B preferably using a bounded model checker. In blocks 112 and 110, synchronous execution, partial order reduction and transactions are incorporated into the framework by statically augmenting the circuit-based boolean encoding of the given concurrent program with additional constraints.
Issues arising out of synchronization primitives and the preservation of temporal properties are handled by treating them as conflicts. Whereas thread local operations can always be executed in parallel, operations on shared variables or those involving synchronization primitives can affect the control flow of both threads and so we need to explore all necessary interleavings of such operations. Such synchronization imposed constraints are captured using the notion of synchronization conflicts in block 112. We note that such synchronization based conflicts may also be used in partial order reduction (POR) in block 110.
Referring to FIG. 2, in block 202, we need to make sure that synchronous execution preserves the behavior of the concurrent program with respect to the given temporal property, f, viz., CPint|=f iff CPsync|=f, where CPint and CPsync denote, respectively, the state transition diagrams of the given concurrent program CP under interleaving and synchronous semantics, and f is a stuttering insensitive temporal logic formula.
We only consider LTL\X (Linear Temporal Logic) formulae to demonstrate the present principles, however other formulae may be employed. Executing a program synchronously changes its semantics. Moreover, each temporal property defines a set of global states and transitions of interest in the given program, viz., states on which its atomic propositions are interpreted to be true and transitions which when executed cause a change in the valuations of atomic propositions appearing in the given temporal property. In block 204, these states and transitions are explored in CPsync.
In block 206, we enumerate all interesting states as temporal conflict pairs. Then, by enforcing a context switch for each temporal conflict pair, we ensure that we do not miss exploring any of these global states of interest in CPsync thereby preserving f. In general, enumerating all temporal conflict pairs directly from the syntax of the given formula f might be cumbersome. However, noting that a Büchi automaton Bf for f captures all the necessary information, we can, capture the information by analyzing Bf and efficiently generate these pairs. Our notion of temporal conflicts is more refined than existing notions of visible transitions used to detect conflicts for POR in that our notion takes into account the temporal structure of the given property as opposed to visible transitions which just track the control states of the given program over which atomic propositions of f are interpreted.
An important consequence is that using temporal conflicts instead of the notion of visible transitions leads to far fewer context switches. Thus, our notion of temporal conflicts can also be seen as a more refined way to compute stubborn sets and thereby enhance POR in addition to leveraging synchronous execution and symbolic model checking.
Having identified the synchronization (202) and temporal conflicts (204, 206), we next compute a minimal set of transitions that need to be explored from each state in block 208. This includes generalizing the standard procedure for computing conditional stubborn sets which handles only synchronization constraints. This permits us to seamlessly integrate partial order reduction with synchronous execution.
Finally, on block 210, we show how to add transactions on-the-fly for which we use the technique presented in V. Kahlon, A. Gupta, and N. Sinha, “Symbolic model checking of concurrent pro-grams using partial orders and on-the-fly transactions.” In CAV, 2006 (hereinafter Kahlon et al.), incorporated herein by reference, that is based on analyzing patterns of lock acquisition as opposed to locksets. This permits us to cut down on the number of interleavings that need to be explored by essentially disallowing certain context switches to increase the granularity of transitions resulting in a reduced state space.
Thus, we have presented a new approach for model checking concurrent programs that combines the power of synchronous execution with symbolic techniques, partial order reduction and on-the-fly transactions while at the same time retaining the flexibility to employ a broad arsenal of model checking techniques—both SAT and BDD-based—for checking not just reachability but a richer classes of linear-time temporal properties.
System Model: We consider concurrent systems comprised of a finite number of processes or threads where each thread is a deterministic sequential program written in a language such as C. Threads interact with each other using communication/synchronization objects like shared variables, locks and semaphores.
Formally, we define a concurrent program CP as a tuple (T, V, R, s0), where T={T1, . . . , Tn} denotes a finite set of threads, V={v1, . . . vm} a finite set of shared variables and synchronization objects with vi taking on values from the set Vi, R the transition relation and s0 the initial state CP. Each thread Ti is represented by the control flow graph of the sequential program it executes, and is denoted by the pair (Ci,Ri), where Ci denotes the set of control locations of Ti and Ri its transition relation. A global state s of CP is a tuple (s[1], . . . , s[n], v[1], . . . , v[m]) εS=C1 x . . . x. Cn x. V1 x . . . x. Vm, where s[i] represents the current control location of thread T1 and v[j] the current value of variable vj. The global state transition diagram of CP is defined to be the standard interleaved composition of the transition diagrams of the individual threads.
Thus, each global transition of CP results by firing a local transition of the form (ai, g, u, bi), where ai and bi are control locations of some thread Ti=(Ci, Ri) with (ai,bi) εRi; g is a guard which is a Boolean-valued expression on the values of local variables of Ti and global variables in V; and u is function that encodes how the value of each global variable and each local variable of Ti is updated. A transition t=(ai, g, u, bi) of thread Ti is enabled in state s iff s[i]=ai and guard g evaluates to true in s. If s[i]=ai but g need not be true in s, then we simply say that t is scheduled in s. We write




to mean that the execution of t leads from states to s to s1. Given a transition tεT, we use proc(t) to denote the process executing t. Finally, we note that each concurrent program CP with a global state space S defines the global transition system AG=(SΔ, s0), where Δ⊂S×S is the transition relation defined by (s, s1)εΔiff ∃tεT:





and s0 is the initial state of CP.

Synchronous Execution: A concurrent process T1(a) and T2(b) accessing shared variable x is shown in the EXAMPLE 1(a) and 1(b).
EXAMPLE 1(a)















foo( ){



  la:g = o;



 2a: bar ( );



 3a: g = 8;



 4a: x = 1;



 5a: bar’ ( ) ;



 6a: Raceo;



}










EXAMPLE 1(b)















goo( ){



  1b: i = 5;



  2b: y = 2;



  3b; car ( );



  4b: x = 1;



  5b: Car’ ( ) ;



6b: Race1 ;



}










Consider the concurrent program CP shown in Examples 1(a) and 1(b), each comprising one of two threads T1 and T2 accessing shared variable x. Assume that x is not accessed by functions bar and car. Suppose that our goal is to detect the data race represented by the labels Race0 and Race1. In other words, we want to decide whether CP satisfies g=EF (Race0^Race1) which it does. Our focus is on the length of witness traces for g as this governs the depth to which the state space of CP needs to be explored to detect the race.
In an interleaved model of computation, the length of a witness for the above data race would be the sum of the lengths of the local computations of the individual threads T1 and T2 leading to locations Race0 and Race1, respectively. However, we note that since functions bar and car do not access any shared variables, each of their statements could be executed in parallel with any statement of the other thread. On the other hand, statements at program locations 4a and 4b both update the same shared variable, because of which we need to explore both of their interleavings. Thus, threads T1 and T2 can be executed synchronously until one of the threads, say T1, reaches control location 4a or 4b.
Now, there are two possible scenarios to consider. Either T1 alone executes 4a or, to account for the other interleaving, T1 waits for T2 to first execute 4b. In the first case, both threads can now again start executing synchronously. Let d1 and d2 be the number of program statements executed locally by T1 and T2, respectively, along a witness global computation of CP for the data race. Then, in the interleaved model the depth of the witness produced would be d1+d2, whereas in the (partially) synchronous execution model, the depth would be the maximum of d1 and d2 plus 1, with the extra step needed to account for the stuttering produced when T1 alone was allowed to execute 4a while exploring the interleavings enforced by the shared variable x.
In the second scenario, T1 has to first wait for T2 to execute 4b after which both threads can start executing synchronously again. In this case, if d4a and d4b are the depths of locations 4a and 4b, respectively, the depth of the witness is Max(d1, d2)+(d4b−d4a), which is still considerably less than d1+d2. Note that we need not have considered the second scenario at all as producing one witness suffices for a given property.
In real-life code, the effect of reduction in bug depth via partial synchronous execution is even more pronounced. This is because in a concurrent program, shared variables are typically accessed in a very small fraction of the total functions. Most of the computation is done thread locally and synchronization with other threads occurs relatively rarely. Thus, by executing the thread local code synchronously, we can get drastic reductions in the depth of witness traces for properties and, as a consequence, in the depth to which the program needs to explored for detecting an error.
One goal, therefore, is to change the interleaving semantics of the given concurrent program CP to a partially synchronous semantics while ensuring that all interleavings enforced by shared variable accesses are explored. One key point, as noted above, is that if in the current global state s, an operation op of thread T1, say, accessing a shared variable x is enabled and if the other thread can, in some future, execute an operation op′ accessing x, then we need to explore both interleavings wherein we either let only T1 execute op first or we let it stutter until T2 executes op′. Such a pair of operations (op, op′) is a synchronization induced conflict and can be formally captured using, e.g., partial order reduction.
Might-be-first-to-interfere: Let op and op′ be two operations on the same object O and s be a reachable state. The relation op op′ (means that op and op′ are conflicting operations. i.e., access a common shared object) holds if there exists a sequence




of transitions in AG such that ∀1≦i≦n:∀op′′ on O used by ti: op and op′′ are independent in state si,tn uses op′, and op and op′ are dependent in sn.

Thus, the above can be formally re-stated as—if in the current global state S, a thread, T1, is executing operation op and there exists an operation op′ of thread T2 such that op op′, then we need to explore both interleavings where we either execute T1 first or we let T1 stall until T2 executes op′. op op′ means op might-be-first-to-interfere with operation op′.
Preserving Temporal Properties: Merely accounting for synchronization conflicts in not sufficient. Synchronously executing a concurrent program reduces bug depths but also changes its semantics. One important consequence is that we need ensure that the given temporal property f is preserved, viz., CPint/=f iff CPsync/=f, where CPint and CPsync denote the transition diagrams of CP with interleaving and synchronous semantics, respectively.
In the previous example (1(a) and 1(b)), suppose that we want to check whether the property g=E(F(1a^2b ^F (6a^6b))) holds. Since the two threads (Ex. 1(a) and Ex. 1(b)) access shared variable x only at locations 4a and 4b, simply executing the two threads synchronously until one of them reaches either of these locations will result in a computation prefixed by the sequence (1a, 2a), (1b, 2b). In this case, CPint/=f but CPsynt/≠f as due to synchronous execution both T1 and T2 exit in 1a and 2a, respectively, simultaneously whereas in order for CP to satisfy f, T1 needs to “wait” at program location 1a until T2 reaches location 2b. To ensure that f holds, we need to also execute the interleaving that forces T1 to wait until T2 executes 2b. Thus, there is now a new kind of ‘conflict’ between the operations at program locations 1a and 2b even though no shared variable is accessed at either location. We refer to such conflicts that are introduced by the temporal property as temporal conflicts. Note that temporal conflicts can arise even when we are model checking simple data race-like properties, e.g., EF(c1^b2), where c1 and b2 are control locations occurring in loops in different threads.
Along a computation satisfying g=E(F(1a^2b^F(6a^6b))), the only relative orderings between pairs of local states that do matter are (1a, 2b), (2b, 1a), (6a, 6b), (6b, 6a). Indeed, since 1a and 2b need to occur together in a global state, if T1 is in local state 1a, we permit an interleaving where T1 waits for T2 to reach 2b, if possible, and vice versa. In general, given an LTL property f, we need to enumerate all possible pairs of (atomic proposition that are) control states occurring in g that can occur together in a computation satisfying Eg. This might be cumbersome looking merely at the syntax of g. However, a Büchi automaton Bg for g captures the necessary information, by encoding all possible models for g. Without loss of generality, we may assume that atomic propositions of g are control states of T1 or T2 or negations thereof. Indeed, any atomic proposition h involving data variables can be converted to an expression involving purely control locations by introducing new program statements with an if condition guarded by h.
In general, each transition tr:




of Bg is labeled with a boolean expression e of atomic propositions of g which, in our case, are control states. Writing e in disjunctive normal form as e=e1 V . . . V ek, we can replace tr with k transitions from a to b with the ith being labeled with ei. Thus, we can assume that e is a conjunction of control states of T1 or T2 or negations thereof. Thus, e is either true or of the form e11^ . . . ^e1k1^e21^ . . . ^e2k2, where eij is a control state of T1 or negation thereof. Transitions labeled with false are dropped. Now we can simply read off the temporal conflict pairs from Bg as pairs of the form (c1, c2), where c1 is a control state of T1 and there exists a transition of Bg labeled with e11^ . . . ^e1k1^e21^ . . . ^e2k2, where for i=1,2, there exists jiε[1 . . . k1] such that eij, is either of the form ci or of the form ci. Intuition behind defining the conflicts is this fashion is to force context switches before and after control states where the valuations of atomic propositions change.

Note that the natural way of defining conflict pairs would be to enumerate all pairs of control locations that satisfy atomic propositions of the given temporal formula. Indeed, if we are given a formula of the form EF(c1^c2), where ci is a control location of Ti, then we would generate all pairs (c1, c′2, where c′2εC2 \{c2}. However, since the cardinality of C2\{c2} is likely to be high, it will generate too many conflict pairs and force too many context switches thus killing the model checking run. Instead, we generate just one conflict pair (c1, c2), which forces a context switch before and after control state c2 of thread T2. In other words, by forcing context switches only at those control locations where the atomic propositions of the given temporal formula change value instead of where they hold true, we can drastically cut down on the number of conflict pairs (and hence context switches) needed while still preserving the given property.
Let TCg be the set of all temporal conflict pairs of g. In defining the synchronous semantics CPsync of CP, we satisfy for each temporal conflict pair (c1, c2)εTCg the constraint that if thread T1 is currently in control location c1 and if T2, could in future reach control location c2, then we need to consider both interleavings where location c1 is executed before c2. A simplified Büchi automaton Bf for g=E(F(1a^2b^F(6a^6b)) is given in FIG. 3. The simplified Büchi automaton of FIG. 3 is labeled in accordance with the example 1(a)/1(b). It can be seen that the set of temporal conflict pairs is {(1a, 2b), (6a, 6b)}. Since (1a, 2b) is a temporal conflict pair, in CPsync, we will be forced to explore the interleaving where T1 waits for T2 to first execute 2b. This ensures that CPsnyc/=f iff CPintc/=f. Indeed, each temporal property defines a set of global states of CP of interest, viz., those on which its atomic propositions are interpreted to be true. The remaining states act as ‘white space’ with respect to the property. By introducing context switching via temporal conflict pairs, we ensure that none of these global states of interest miss exploration in CPsync.
Given TCg, we can, as for constraints arising out of synchronization primitives, capture temporal constraints using a temporal might-be first-to interfere relation 
Temporal-Might-be-first-to-interfere: If op and op′ are two operations at locations c and d of T1 and T2, respectively, (not necessarily on the same object) with (c, d)εTCg, and s a reachable state, the relation opop′ holds if there exists a sequence




of transitions in AG such ∀1≦i<n: for control location c′′ at ti: (c, c′′)∉TCg and the control location at tn is d.

The issue of tracking temporal conflicts also arises when partial order reduction is applied in the model checking of a general LTL temporal formula f. Techniques have been proposed for addressing this problem which can, broadly speaking, be classified into two categories based on whether the synchronization of the Büchi automaton Bf for the given temporal property f with the system to be verified is based on states or on actions labeling transitions.
In the present case, properties are interpreted over control states of threads in the given concurrent program. For such a framework, where the synchronization of Bf with the given program is state based, temporal conflicts have traditionally been incorporated using the notion of visibility of transitions. A transition is said to be visible if executing it affects at least one proposition in the given temporal property f—the intuition being that only the firing of such transitions can affect the valuation of f. Thus, techniques for computing persistent sets (including the known stubborn set and ample set methods) based on the notion of visible transition will declare a (temporal) conflict between each pairs of control states c1 and c2 of threads T1 and T2, respectively, where c1 and c2 both appear in f. However, this notion of visibility is too coarse as it ignores the structure of the given temporal property. This temporal insensitivity can result in too many context switches as is illustrated by the following example 2.
EXAMPLE 2
Concurrent Program with Threads T1(2(a)) and T2 (2(b))
















foo( ){
goo( ){



 1a: x = 0;
 1b: p = 0;



 2a: for (i = 0; i < 1000; i++)
 2b: q = 1;



 3a: y++ ;
 3b: r = 2;



 4a: x = 1
 4b: t = 0;



}
}



  T1: 2(a)
 T2: 2(b)










Suppose that we want to check whether the property f=E(1a^4b^F(3a^F(4a))) holds at the initial state of the program comprised of two threads executing functions foo and goo shown in Example 2. Using the notion of visibility, we see that each of the locations 1a, 3a and 4a conflict with 4b. During BMC, when the loop in unrolled 1000 times it will end up producing 1000 conflicts between 3a and 4b thus resulting in too many context switches. However, since the only temporal conflict pair given by the Büchi Automaton is (1a, 4b), we will introduce only 1 conflict. Indeed, only 1a and 4b need occur together for the property to be satisfied. There are no such constraints on other control locations. Note that depending on the atomic propositions the number of context switches might easily blow up for a large program if one uses the standard notion of visibility. Thus, the notion of temporal-might-be-first-to-interfere, in accordance with the present principles, is more refined as it takes the structure of the temporal property into account using information gleaned from its Büchi automaton, thereby resulting in much lesser context switches.
Thus, even though the original goal was to leverage synchronous execution semantics and not POR, our notion of temporal conflicts can also be seen as a more refined way to compute ample and stubborn sets and thereby enhance POR in addition to leveraging synchronous execution and symbolic model checking.
An orthogonal technique for reducing conflicts that leverage formula structure is given in the prior art. The boolean operators in the given temporal formula are driven upwards in the formula as far as possible using the distributive properties of temporal operators with respect to boolean connectives. Then, if the original formula f is rewritten as a boolean function of the subformulas f1, . . . , fn it suffices to compute conflicts individually over each sub-formula fi instead of the entire formula f. Since one does not need to compute conflicts across the subformulas, there can be a significant reduction in the total number of conflicts for f in accordance with the present principles.
In the framework where synchronization between the Büchi Automaton Bf and a given system is done via actions, the standard approach is to treat Bf just like any other process. This technique implicitly incorporates the structure of the given temporal property in the detection of temporal conflicts to a greater extent than the one based on visible transitions. However, as discussed before, to prevent unnecessary context switches, care must be taken even here to involve only those transitions that change the valuations of atomic propositions of the given formula instead of those that merely access control states appearing in the given formula.
Synchronous Execution+POR+Transactions: Partial-order reduction (POR) exploits the fact that concurrent computations are essentially partial orders on operations of threads on communication objects, and hence, we need not explore all interleavings of operations of threads comprising a given concurrent program that realize this partial order—but only a few. In practice, this reduction is realized by exploring from each state only those transitions that belong to a persistent set of that state instead of all the enabled transitions. A persistent set for a global state s of CP captures a minimal set of transitions that need to be explored from each global state of the given concurrent program in order to ensure that all necessary interleavings induced by synchronization primitives are explored.
Partial order reduction based on temporal conflicts takes into account only the constraints arising out of synchronization primitives but not the temporal constraints. Capturing these synchronization constraints via the  relation then leads to computing conditional stubborn sets. For this, dependencies between transitions, arising out of operations on shared communication objects are captured using the  relation which encodes for each operation op used by a transition in a state s which other operations might be first to interfere with op from the current state s.
For synchronous execution, we have to additionally incorporate temporal constraints as discussed previously. This can be easily accomplished by defining a new dependency relation that is the union of the might-be-first-to-interfere relation  (captures synchronization conflicts) and temporal-might-be-first-to-interfere relation  (captures temporal conflicts). This leads to a new method as shown in example 3 to compute (an over-approximation of) persistent sets. For each local transition




or a thread, we let used(t) denote the set of operations on variables and synchronization objects executed during the execution of t.

EXAMPLE 3
Method for Computing Conditional Stubborn Sets


    1. Initialize Ts={t}, where t is some enabled transition in s.
    2. For each






    
    
        (a) add to Ts all transitions t′ such that proc(t)≠proc(t′) and opεused(t), op′εused(t′): op op′.
        (b) If t is disabled in s,
        
            i. if Tj=poc(t) and s[j]≠a, then add to Ts all transitions t′ of Tj of the form
        
        
    
    






or

    
    
        ii. choose a condition cj in the guard g of t that evaluates to false in s; then, for all operations op used by t to evaluate cj, add to Ts all transitions t′ such that op′. used(t′): opop′.
        (c) If t is enabled in s add to Ts all transitions t′ such that
        
            i. proc(t)≠proc(t′) and opεused (t), op′εused(t′): opop′.
        
        
    
    
    3. Repeat step 2 until no more transitions can be added in Ts. Then return all transitions in Ts, that are enabled in s.


Note that for computing conditional stubborn sets in step 2a, where we include in Ts, transitions that are temporally dependent with some transitions in Ts. Due to this step, extra transitions capturing temporal constraints are added to Ts resulting in a superset of a persistent set. As discussed above, these extra transitions are needed to preserve the property being checked during synchronous execution which was not an issue in partial order reduction.
Leveraging Lock Acquisition Patterns for On-the-fly-Transactions: Determining the relations , and  precisely would need an exploration of the state space of the program at hand, which is precisely what we want to avoid. Therefore, in practice, we employ static analysis to compute over-approximations of relations , and  Towards that end, we say that two operations op and op′ are statically dependent if they access a common shared variable such that at least one of the accesses is a write operation. In Kahlon et al., it was shown that in statically determining , one could also incorporate transactions by making use of the semantics of locks to enforce mutual exclusion. This permits us to reduce the number of context switches among threads and hence the state space that needs to be explored, it was shown that by tracking lock acquisition patterns instead of merely locksets one can identify provably large transactions. The over-approximation  for  is given below.
Definition (might-be-the-first-to-interfere-modulo-lock-acquisition) Let op and op′ be two operations on a common shared variable and s a reachable state of AG. The relation op′ holds iff there exist distinct threads Ti and Tj such that there exists (1) a transition of Ti scheduled (not necessarily enabled) at s using op, and (2) a local path




of T2 such that ∀1≦k<n:∀op′′ used by tk: op and op′′ are not statically dependent, tn uses op′, and op and op′ are statically dependent and no lock held by Ti in s is acquired by Tj along x.

Analogously, we can statically define an over-approximation  that also takes into account lock acquisition patterns for identifying larger transactions.
Definition (temporal-might-be-the-first-to-interfere-modulo-lock-acquisition) Let op and op′ be two operations at control locations c and d of threads T1 and T2 such that (c, d)∈TCg, where TCg is the set of conflict temporal pairs for the given property Eg, and let s be a reachable state of AG. The relation op op′ holds iff there exists (1) a transition of T1 scheduled (not necessarily enabled) at s using op. and (2) a local path x:




of T2 such that (i) the control state of T2 in pn is d, (ii) ∀1≦k≦n::(c,c′)∉TCg where c′ is the control state of T2 in tk, and (iii) and no lock held by T1 in 5 is acquired by T2 along x.

Now replacing the usage of  and  in the above algorithm with  and  respectively, allows us to statically compute the transitions that need be explored from each global state under both synchronization and temporal constraints.
Synchronous Modeling for Concurrent C Programs:
Translating Individual Threads into Circuits: (See e.g., FIG. 1, block 102 and 104.) We first obtain a circuit-based model for each thread, under the assumption of bounded data and bounded control (recursion). Towards that end, we view a control flow graph (CFG) of each thread of the given program as a finite state machine with state vector (pc, V), where pc denotes an encoding of the thread locations, and V is a vector of integer-valued program variables. We construct a symbolic representation of these transition relations resembling a hardware circuit. For the pc variable, we allocate [logN] latches, where N is the total number of thread locations. For each C thread variable, we allocate a vector of n latches, where n is the bit width of the variable. A circuit-based model for each thread of the given concurrent program, is then built where each variable of the thread is represented in terms of a vector of binary-valued latches and a Boolean next-state function (or relation) for each latch. See Kahlon et al. for details.
Building the Circuit for the Concurrent Program: Given the circuit Ci for each individual thread Ti, we now show how to get the circuit C for the concurrent program CP comprised of these threads. In the case where local variables with the same name occur in multiple threads, to ensure consistency, we prefix the name of each local variable of thread Ti with thread_i. Next, for each thread Ti, we introduce a gate execute_i indicating whether Pi has been scheduled to execute in the next step of CP or not.
For each latch l, let next-statei (l) denote the next state function of l in circuit Ci. Then in circuit C, the next state value of latch thread_i_l corresponding to a local variable of thread Ti, is defined to be next-statei(thread_i_l) if execute_i is true, and the current value of thread_i_l, otherwise. If, on the other hand, latch l corresponds to a shared variable, then next-state(l) is defined to be next-state(l), where execute_i is true. Next, we implement a scheduler which determines in each global state of CP which of the signals execute_i is set to true and thus determines the semantics of thread composition.
POR+Synchronous Execution:
Referring to FIG. 4, to incorporate/integrate synchronous execution and partial order reduction, we need to ensure that from each global state s, only transitions belonging to (an over-approximation of) a conditional stubborn set of s as defined above are explored in block 402. Let R and Ri denote the transitions relations of CP and Ti, respectively. Since CP has two threads, we introduce the 2-bit vector cstub where cstubi is true for exactly those threads Ti such that the (unique) transition of Ti enabled at s belongs to the same minimal over-approximation of a conditional stubborn set of s as identified by the Example 3 method. Then:




  
    R
    ⁡
    
      (
      
        s
        ,
        
          s
          ′
        
      
      )
    
  
  =
  
    ⋀
    
      
        i
        =
        1
      
      ,
      2
    
  




(executed_i cstubi(s) ^Ri(s,s′)).

In block 404, the cstub vector can be computed in the following way:
In block 406: For each shared variable a, and thread Ti, we introduce a latch touch-now(Ti,x) which is true at control location pci of Ti iff Ti accesses x at control location pci. This can be done via a static analysis of the CFG of Ti by determining at which control locations x was accessed and taking a disjunction for those values of pci.
In block 408: For each shared variable x and thread Ti, introduce the latch touch-now-later (Tj, x), which is true at control location pcj of Tj if Tj accesses x at some location pc′j reachable from pcj. Thus, computing touch-now-later (Tj, x) involves deciding the reachability of pcj, and since we cannot compute it exactly without exploring the entire state space AG of CP, we over-approximate it by doing a context-sensitive analysis of the control-flow graph of Tj. We set touch-now-later-pair (Tj, x) to true in control pcj if for some control pc′j reachable from pcj in the control flow graph of Tj, x is accessed at pc′j.
In block 410: For distinct threads Ti and Tj, the relation synch-conflicti (j) is then defined as VxεVsh (touch-now (Tj, x) (pci) A touch-now-later (Tj, x) (pcj)), where pci and pcj are the control locations of Ti and Tj, respectively, in the current global state and Vsh is the set of shared variables of CP.
In block 412: For distinct threads Ti and Tj, the relation temp-conflict(j) is defined as V(ci,cj)εTCg, ((pci=ci) ^Reachable (pcj, cj), where TCg is the set of temporal conflict pairs of the given property Eg, and Reach (pcj, cj) is true if cj is reachable from pcj. An over-approximation for Reach (pcj, cj) is determined statically.
In block 414: Define conflicti (j)=synch-conflictj(j) V temp-conflicti(j).
In block 416: Using a circuit to compute transitive closures, for each i, starting with Ji={i} we compute the closure of J1 . . . Jn under the conflict relation defined above.
In block 418: We build a circuit to compute the index min such that the cardinality of Jmin is the least among the sets J1 . . . Jn Finally, ∀1≦i<n, set cstubi=1 iff iεJmin. Note that in the implementation we need to pick only one set with the least cardinality.
Cycle detection: Detection of cycles is handled as described in Kahlon et al. Our experience also has been that acyclic state spaces are very common in software implementations for the purpose of model checking and cycle detection and become more critical when one is using an abstraction (which introduces cycles) refinement framework. However, since (i) we put a lot of effort in modeling programs concretely, (ii) do not use abstraction refinement, and (iii) introduce sticky transitions to cover common trivial cases, the impact of the existence of cycles is reduced.
Encoding Lock Pattern based Reductions: To incorporate transactions on-the-fly, we augment the predicate touch-now-later, to generate the new predicate touch-now-later-LS that also includes lock acquisition pattern information. For control locations pci and pc′i, of thread Ti, let paths (pci,pc′i) denote the set of paths in the CFG of Ti starting from pci that may reach pc′i. For each n E paths(pci,pc′j) of Ti, let lockPred(π) be a formula denoting the set of locks (lk) acquired (and possibly released) along π, e.g., lk1=Ti^lk2=Ti. Let touch-not-later-pair(Tj,x) (pcj, pcj) encode all possible sets of locks that can potentially be acquired along local paths in Ti from pci to pc′i accessing x, i.e., touch-now-later-pair(Tj,x) (pcj,pcj) touch-now (Tj,x) (pc′j) ^AP (pcj,pc′j) where AP(pci,pc′i)=Vπεpaths(pci,pc′i) lockPred(π). Let CLP(Ti, s) denote a formula encoding the ownership of locks by Ti in global state s. Then, the relation touch-now-LS(Ti, x) is obtained from touch-now-later-pair(Ti, x) by quantifying out pc′i and conjoining with the CLP(Ti,s), i.e., touch-now-LS(Ti, x) (pci)=(∃pc′i touch-now-later-pair (Ti, x) (pci, pc′i) ^CLP(Ti,s). Thus, touch-now-LS(Ti, x) (pci) is true if there is a location pci accessing shared variable x that is reachable from pci via a local path π in Ti such that no lock held in s is acquired along n. We evaluate lockPred(π) using a context sensitive static analysis of the CFG of Ti. The temp-conflict relation is modified analogously. Here, temp-conflicti(j)=V(ci, cj)εTCg ((pci=ci)^AP(pcj, cj) ^CLP(T1, s)).
The Daisy Case Study: We have used our technique to find bugs in the Daisy file system which is a benchmark for analyzing the efficacy of different methodologies for verifying concurrent programs. Daisy is a 1KLOC Java implementation of a toy file system where each file is allocated a unique inode that stores the file parameters and a unique block which stores data. An interesting feature of Daisy is that it has fine grained locking in that access to each file, inode or block is guarded by a dedicated lock. Moreover, the acquire and release of each of these locks is guarded by a ‘token’ lock. Thus, control locations in the program might possibly have multiple open locks and furthermore the acquire and release of a given lock can occur in different procedures. We have shown the existence of the race conditions described below also noted by other researchers.
Memory is a more critical bottleneck in model checking than time. Since usage of synchronous execution clearly leads to a significant reduction in the memory usage, it permits us to (a) handle larger programs, and (b) explore programs to a greater depth than we otherwise could. Usage of synchronous execution reduces the witness depth and as a result the memory usage which depends on the unroll depth of the BMC.
In accordance with useful embodiments, we add constraints so that we explore a conditional stubborn set at each global state thereby yielding considerable state space reduction. The present approach adds information to the model while exploring the state space by detecting dependencies on-the-fly via an analysis of patterns of lock acquisition. Our more refined method generates fewer dependencies between transitions resulting in a lesser number of context switches. This gives us better state space reduction than existing lockset based techniques.
We have presented a new approach for verifying concurrent programs that combines the power of synchronous execution and symbolic techniques with partial order reduction and on-the-fly transactions, while retaining the flexibility to employ a variety of error trace generation/proof techniques—both SAT and BDD-based—for checking not just safety but a broad class of linear time temporal properties. We have also introduced temporal conflicts which enables us to improve partial order reduction techniques by allowing us to compute smaller stubborn sets. Finally, there has been considerable research devoted recently to the parallelization of model checking in order to ensure greater scalability. Since the issues that arise in distributed model checking are precisely those as encountered during synchronous execution, we believe that the notion of temporal conflicts can play a crucial role in distributed model checking.
Having described preferred embodiments of a system and method for accelerating model checking via synchrony (which are intended to be illustrative and not limiting), it is noted that modifications and variations can be made by persons skilled in the art in light of the above teachings. It is therefore to be understood that changes may be made in the particular embodiments disclosed which are within the scope and spirit of the invention as outlined by the appended claims. Having thus described aspects of the invention, with the details and particularity required by the patent laws, what is claimed and desired protected by Letters Patent is set forth in the appended claims.

## Claims

1. A computer implemented method for program verification by via bounded or unbounded model checking in concurrent programs, comprising:
modeling each of a plurality of program threads as a circuit model;
generating a full circuit for an entire program by combining the circuit models including constraints which enforce synchronous execution of the program threads; and
verifying the program using the synchronous execution to reduce the amount of memory needed to verify the program and a number of steps taken to uncover an error; wherein using the synchronous execution includes determining synchronous conflicts conflicts to determine the subset of transitions that must be explored from each global state.

2. The method as recited in claim 1, further comprising leveraging synchronous execution to reduce,the depth of computations explored during model checking.

3. The method as recited in claim 1, wherein verifying includes:
checking necessary interleavings induced by shared variable updates and synchronization primitives by switching from interleaving to synchronous semantics while preserving a temporal property being model checked; and
integrating synchronous execution with partial order reduction, transactions and symbolic model checking.

4. The method as recited in claim 1, wherein using the synchronous execution includes determining synchronous conflicts.