计算机数理逻辑-程序验证-并发程序

Verification is routinely used when developing computer hardware and concurrent programs. A sequential program can always be tested and retested, but the nondeterministic nature of hardware and concurrent programs limits the effectiveness of testing as a method to demonstrate that the system is correct. Slight variations in timing, perhaps caused by congestion on a network, mean that two executions of the same program might give different results. Even if a bug is found by testing and then fixed, we have no way of knowing if the next test runs correctly because we fixed the bug or because the execution followed a different scenario, one in which the bug cannot occur.

在开发计算机硬件和并发程序时，经常会用到验证。一个顺序程序总是可以被测试和重新测试，但硬件和并发程序的非确定性限制了测试作为证明系统正确的方法的有效性。时间上的微小变化，也许是由网络上的拥堵造成的，意味着同一个程序的两次执行可能会得到不同的结果。即使通过测试发现了一个错误，然后进行了修复，我们也没有办法知道下一次测试的正确运行是因为我们修复了这个错误，还是因为执行了一个不同的场景，在这个场景中，这个错误不会发生

  • 顺序程序的验证貌似没有用到时态逻辑

1. Concurrent Program 并发程序

  • A concurrent program is a set of sequential programs together with a set of global variables
  • A concurrent program is a set of processes ${ p_1,p_2,…,p_n }$, where each process is a sequential program
    • Processes are also known as threads; in some contexts, the two terms have different meanings but the difference is not relevant here
      • 进程与线程在此处无需区别
  • The variables declared in each process are its local variables; a local variable can be read and written only by the process where it is declared.
  • There may be global variables that can be read and written by all of the processes.

1.1. state 状态

  • The state of a concurrent programs consists of
    • the values of its variables (both local and global),
    • together with the location counters of its processes.

Example

There are $5×3×3=45$ different states, because the variable n can have the values $0, 1, 2, 3, 4$ and there are three labels for each process.

  • These seems like quite a large number of states for such a simple program, but many of the states (for example, (0,end,end)) will never occur in any computation.
  • possible computations:

1.2. Interleaving 交错

  • A computation of a concurrent program is obtained by asynchronous interleaving of atomic instructions
    • 并发程序的计算是通过原子指令的异步交错得到的
  • Each statement is executed to completion before the execution of another statement (from the same process or another process) is started
    • these statements are atomic operations

2. Formalization of Correctness

  • Correctness properties of concurrent programs can be expressed in linear temporal logic.
  • There are two types of properties:
    • safety properties that require that something bad never happens
    • liveness活泼 properties that require that something good eventually happen.
  • Each process consists of a critical section and a non-critical section.
    • A process may stay indefinitely in its non-critical section, or—at any time—it may request to enter its critical section.
    • A process that has entered its critical section will eventually leave it
    • Mutual exclusion: It is forbidden for the two processes to be in their critical sections simultaneously.
    • Liveness: If a process attempts to enter its critical section, it will eventually succeed

2.1. Peterson’s algorithm 彼得森算法

  • The statement: wait until (!wantq or turn == 2) is a more intuitive way of writing:
    • while (!(!wantq or turn == 2)) /* do nothing */
  • The variables wantp and wantq are set to true by the processes to indicate that they are trying to enter their critical sections and reset to false when they leave their critical sections.
  • A trying-process waits until the other process is neither trying to enter its critical section nor is it in its critical section (!wantq or !wantp). Since the algorithm is symmetric, the variable turn is used to break ties when both processes are trying to enter their critical sections.
  • A tie is broken in favor of the first process which set turn. Suppose that process p set turn to 1 and then process q set turn to 2. The expression turn==2 will be true and allow process p to enter its critical section.
  • The following two LTL formulas express the correctness of Peterson’s algorithm for the critical section problem:
  • cs = critical section
  • Mutual exclusion forbids (always false) a computation from including a state where both processes are in their critical section,
  • while liveness requires that (always) if a computation includes a state where a process is trying to enter its critical section then (eventually) the computation will include a state where the process is in its critical section.

2.2. progress axioms

2.3. Invariants 不变量

  • $r$ is invariant, meaning that $r$ is true initially and remains true in any interpretation
  • deduction rule:

3. Programs as Automata – model checking

  • There is a different approach to the verification of the correctness of a program: generate all possible computations生成所有可能的计算 and check that the correctness property holds for each of them. Of course, this is possible only if there are a finite number of states so that each computation is finite or finitely presented. 所基于的假设
    • For the program for integer square root整数平方根的程序, we could prove its correctness this way for any specific value of a, but we could not prove it in general for all values of a.
    • However, many concurrent algorithms have a finite number of states
  • This approach to verification is called model checking.
    • A concurrent system is represented by an abstract finite model that ignores details of the computation
    • a correctness property is expressed as a formula (usually in temporal logic) and we wish to show that the program is a model解 of the formula, that is, an interpretation in which the formula is true

3.1. Modeling Concurrent Programs as Automata

  • Concurrent programs can be modeled as finite automata有限自动机

    • Each value of the location counter is a state of one of the automata
    • while each transition is labeled with the Boolean condition that enables it to be taken or with the assignment statements that change the values of the variables.

  • 相比之下，顺序程序的correctness是通过 inductive expressions ${ p }S{ q }$来表示的

  • The abbreviated简略的 version of Peterson’s algorithm

  • The automata for the individual processes do not define the entire concurrent program. We must combine these automata into one automaton(automata的复数形式)
  • The states are defined as the Cartesian product of the states of the automata for the individual processes.

3.2. The State Space 状态空间

The reachable states of a concurrent program are the states that can actually occur in a computation. The state space of the program is a directed graph:

  • each reachable state is a node
  • and there is an edge from state $s_1$ to state $s_2$ if some transition of the program which is enabled in $s_1$ moves the state of the computation to $s_2$.

 

  • State space for Peterson’s algorithm

4. Model Checking of Invariance Properties

We now consider the second meaning of the term model: Is the state space a model of a correctness property? Consider the correctness property for mutual exclusion in Peterson’s algorithm $A=□¬ (csp∧csq)$ . Since the state spacerepresents all the reachable states and all the transitions between them, any interpretation for $A$ must be an infinite path in this directed graph. A quick inspection of the graph shows that all of the ten reachable states satisfy the formula $¬ (csp∧csq)$; therefore, for any interpretation (that is, for any path constructed from these states), $□¬ (csp∧csq)$ is true.

Once we have written the program and the correctness property, there are algorithms to perform the rest of the proof:

  • compile the program to a set of automata
  • construct the product automaton
  • generate the state space
  • check the truth of the formula expressing the correctness property at each state.

4.1. Algorithms for Searching the State Space

  • breadth-first search (BFS)
  • depth-first search (DFS)

5. Model Checking of Liveness Properties

  • Using negation, we have: the correctness property does not hold iff there exists a computation is which ¬ A is true, where:
    • $\lnot A \equiv \lnot □ \lnot (csp \land csq) \equiv ◊ (csp \land csq)$
  • The model checking algorithm ‘succeeds’ if it finds a computation where ¬ A is true; it succeeds by finding a counterexample proving that the program is incorrect.
  • The states on the stack of a depth first search form a path. If the construction ever tries to generate a state that already exists higher up on the stack, the transition to this node defines a finitely-presented infinite computation like the ones shown above.
  • we could generate the entire state space and then check each distinct path to see if it model, but it is more efficient if the checking can be done on-the-fly即时完成 as we did for safety properties. The key is to transform an LTL formula into an automaton whose computations can be generated at the same time as those of the program.

6. Expressing an LTL Formula as an Automaton

  • An LTL formula can be algorithmically transformed into an automaton that accepts an input if and only if the input represents a computation that satisfies the LTL formula.
  • The automaton is a non-deterministic Büchi automaton (NBA), which is the same as a non-deterministic finite automaton (NFA) except that it reads an infinite string as its input and its definition of acceptance is changed accordingly
  • 在计算理论中，非确定有限状态自动机或非确定有限自动机是对每个状态和输入符号对可以有多个可能的下一个状态的有限状态自动机。这区别于确定有限状态自动机，它的下一个可能状态是唯一确定的
  • the negation of the liveness formula
    • $\lnot □A ≡ \not □(waitp→◊csp) ≡ ◊(waitp \land □ \not csp)$
  • The intuitive meaning of the formula is that the computation can do anything (expressed as true), but it may nondeterministically decide to enter a state where waitp is true and csp is and remains false from then on. Such a computation falsifies the liveness property.
  • In state $s_1$, if csp ever becomes true, there is no transition from the state; as with NFA, an automaton that cannot continue with its computation is considered to have rejected its input

7. Model Checking Using the Synchronous Automaton

On-the-fly model checking for an invariance property simply evaluates the correctness property as each new state is generated

When checking a liveness property (or a safety property expressed in LTL as $□A$), every step of the program automaton—the asynchronous product automaton of the processes—is immediately followed by a step of the NBA corresponding to the LTL formula expressing the negation of the correctness property. The product of the asynchronous automaton and the NBA is called a synchronous automaton since the steps of the two automata are synchronized.

7.1. Model checking the liveness of Peterson’s algorithm

  • Starting from the initial state 1, state 2 is reached and $◊(waitp∧□¬ csp)$ will be true, provided that we can find a reachable MSCC（强连通分量，Strongly connected component）where $¬ csp$ holds in all its states.
  • A nested DFS is initiated. Clearly, states 4 and 8 cannot be part of the MSCC since ¬ csp is false in those states
  • the computation can continue: $1,2,5,5,…$ and the state 5 with its self-loop forms an MSCC such that $¬ csp$ is false in all its states
    • rejected
  • Continuing the DFS, we encounter two more states 6 and 9 where waitp is true. We leave it as an exercise to show that the nested DFS will find computations in which ¬ csp holds in all states, but that these computations are also unfair. Therefore, the liveness holds for Peterson’s algorithm

7.2. Fair

  • A computation is (weakly) fair if a transition that is always enabled is eventually executed in the computation.
  • The statement wait until (!wantq or turn == 2) is always enabled because turn=2, but it is never taken. Therefore, we reject this counterexample

8. Branching-Time Temporal Logic

.

9. Symbolic Model Checking 符号模型检验

  • In symbolic model checking, the states and transitions are not represented explicitly; instead, they are encoded as formulas in propositional logic
    • 在符号模型检查中，状态和转换没有明确表示；相反，它们被编码为命题逻辑的公式

exampl

  • A state in the state space of Peterson’s algorithm can be represented as a propositional formula using five atomic propositions.

    • There are three locations in each process, so two bits for each process can represent these values ${p_0,p_1,q_0,q_1}$
    • The variable turn can take two values so one bit is sufficient. The atomic proposition t will encode turn: true for turn=1 and false for turn=2

  • The initial state of the state space is encoded by the formula:

    • $p_0 \land p_1 \land q_0 \land q_1 \land t$

  • To encode the transitions, we need another set of atomic propositions:

    • the original set will encode the state before the transition
    • and the new set (denoted by primes) will encode the state after the transition

  • The encoding of the transition from $s_5=(waitp,waitq,2)$ to $s_8$ is given by the formula:

  • There are two ways of proceeding from here

    • One is to encode the formulas using BDDs
      • The algorithms on BDDs can be used to compute the formulas corresponding to new sets of states: union, predecessor, and so on
    • The other approach to symbolic model checking is called bounded model checking.
      • Recall that a formula in temporal logic has the finite model property: if a formula is satisfiable then it is satisfied in a finitely-presented model. For an LTL formula, we showed that a model consists of MSCCs that are reachable from the initial state. In fact, by unwinding解开 the MSCCs, we can always find a model that consists of a single cycle reachable from the initial state
      • In bounded model checking, a maximum size $k$ for the model is guessed. The behavior of the program and the negation of a correctness property are expressed as a propositional formula obtained by encoding each state that can appear at distance $i$ from the initial state $0≤i≤k$. This formula is the input to a SAT solver; if a satisfying interpretation is found, then there is a computation that satisfies the negation of the correctness property is true and the program is not correct.

9.1. BDD 二元决策图

( 二元决策图 Binary decision diagram)

A binary decision diagram (BDD) is a data structure for representing the semantics of a formula in propositional logic. A formula is represented by a directed graph and an algorithm is used to reduce the graph.

  • 二元决策图（BDD）是一种数据结构，用于表示命题逻辑中一个公式的语义。一个公式由一个有向图表示，并使用一种算法来减少该图。

A Boolean function can be represented as a rooted, directed, acyclic graph, which consists of several (decision) nodes and two terminal nodes. The two terminal nodes are labeled 0 (FALSE) and 1 (TRUE). Each (decision) node ${\displaystyle u}$ is labeled by a Boolean variable ${\displaystyle x_{i}}$ and has two child nodes called low child and high child. The edge from node ${\displaystyle u}$ to a low (or high) child represents an assignment of the value FALSE (or TRUE, respectively) to variable ${\displaystyle x_{i}}$. Such a BDD is called ‘ordered’ if different variables appear in the same order on all paths from the root. A BDD is said to be ‘reduced‘ if the following two rules have been applied to its graph:

  • Merge any isomorphic subgraphs.
  • Eliminate any node whose two children are isomorphic.
  • In the figures below, dotted lines represent edges to a low child, while solid lines represent edges to a high child.
    • For function ${\displaystyle f(x1,x2,x3)}$, to find ${\displaystyle f(0,1,1)}$, begin at x1, traverse down the dotted line to x2 (since x1 has an assignment to 0), then down two solid lines (since x2 and x3 each have an assignment to one). This leads to the terminal 1, which is the value of ${\displaystyle f(0,1,1)}$
  • The binary decision tree of the left figure can be transformed into a binary decision diagram by maximally reducing it according to the two reduction rules. The resulting BDD is shown in the right figure.