# An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks

Authors: Long Zhang; Wanxia Qu; Yinjia Huo; Yang Guo; Sikun Li
Journal: Wireless Communications and Mobile Computing
 (2018)

---

## Abstract

This paper focused on the safety verification of the multithreaded programs for mobile crowdsourcing networks. A novel algorithm was proposed to find a way to apply IC3, which is typically the fastest algorithm for SAT-based finite state model checking, in a very clever manner to solve the safety problem of multithreaded programs. By computing a series of overapproximation reachability, the safety properties can be verified by the SAT-based model checking algorithms. The results show that the new algorithm outperforms all the recently published works, especially on memory consumption (an advantage that comes from IC3).


---

## Body

## 1. Introduction

The mobile crowdsourcing network is a promising network architecture to perform tasks with human involvement and numerous mobile devices but suffers from security and privacy concerns [1, 2]. Pthread-style multithreaded programs play an important role in crowdsourcing computing [3, 4] and crowdsourcing sensing [5, 6] for supporting concurrent programming. Multithreaded programming used much existing system-level code such as device drivers, operating system, and distributed computing. The mobile crowdsourcing networks [7, 8] distribute tasks and collect the results and must make sure safely access for the shared data. Therefore, it is important to verify the safety properties for multithreaded programs.In this paper, we consider the multithreaded programs with an unbounded number of threads. Each thread executes a finite, nonrecursive state machine. Mutexes, which can be expressed using Boolean variables, are used for synchronization in this kinds of multithreaded programs. The illegal access of mutexes will lead to safety problem. We assume all mutexes are shared variables. The safety problems is to verify if the illegal access of mutexes exists.The safety property for multithreaded programs which was expressed as upward-closed sets of the target (“bad”) states can be verified by reduction to the coverability problem ofwell-structured transition systems (WSTS) [9, 10]. WSTS are a very broad class of infinite-state systems, including thread transition system (TTS) [11], Petri nets and their monotonic extensions [12–16], broadcast protocols [17, 18], lossy channel systems [19] and context-free grammars [10]. Coverability is the base verification task for WSTS: the question is whether the system can reach an unsafe or illegal configuration among some subset of its (possibly unbounded number of) components. There have been several algorithms published for WSTS coverability problem [9–11, 20–22], but none perform as efficiently as finite state model checking.The IC3 algorithm [23] is an SAT-based model checking algorithm and introduced as an efficient technique for safety properties verification of finite state systems, especially in hardware verification. It computes an inductive invariant by maintaining a sequence of overapproximation of reachability from initial states and strengthens them incrementally. An efficient implementation of the procedure shows good performance on hardware benchmarks [24].This paper focuses on the multithreaded programs for mobile crowdsourcing networks. All multithreaded programs are pthread-style ANSI-C source code and transformed into TTS by using predicate abstraction [25, 26]. We introduce a novel, highly efficient algorithm for the coverability problem of TTS. The new algorithm is to find a way to apply conventional, finite state IC3, which is typically the fastest algorithm for finite state model checking, in a very clever manner to solve the coverability problem. IC3 algorithm is a finite state model checking algorithm, and the original input is an FSM. We try to use the finite state model checker to solve the infinite-state systems. The bounded TTS is transformed into an FSM and described as the inputs format for IC3 engine. The significant contributions of this paper are as follows:(1)
Our approach requires very novel and intricate reasoning because IC3 produces a series of overapproximation reachability results. A novel algorithm which is based on IC3 engine is proposed to solve the coverability problem of TTS.(2)
We introduce new encoding techniques to make the verification of infinite-state systems possible by using finite state algorithms.(3)
We implement tool’s combination, which is a good way to improve the total rate of successfully solved instances.The experimental results show that our new algorithm outperforms all the recently published works, uses far less memory (an advantage that comes from IC3), and can solve more benchmarks successfully. The new method can solve 97.2% instances within 1 GB.The rest of this paper is organized as follows. In Section2, we review the related work. Section 3 presents necessary preliminaries used in this paper. In Section 4, we propose our new method based on IC3 and give more details of the implementation. Section 5 shows the experimental evaluation on multithreaded programs. Section 6 concludes this paper and discusses future works.


## 2. Related Works

A general decidability result showed that the coverability problem is decidable for WSTS [9], which backward-explore states starting from the target states. Bingham and Hu [20] proposed a new algorithm to compute fix-points over a series of finite state systems of increasing size. A new subclass of WSTS, named Nice Sliceable WSTS, was introduced. Starting from the target states, it computed the exact backward reachability by using finite state symbolic model checking [27] based on BDDs [28] to solve the coverability problem of NSW. Kaiser et al. [11, 22] introduced a new algorithm to solve the safety properties of multithreaded programs with an unbounded number of threads executing a finite state, nonrecursive procedure. By using many inexpensive uncoverability proofs, this new approach combined forward propagation under-approximations with backward propagation of overapproximations to the coverability problem in TTS. Inspired by the success of IC3 algorithm in finite state model checking, Kloos et al. [21] proposed an incremental, inductive procedure to check coverability of downward-finite WSTS, which contains Petri nets, broadcast protocols, and lossy channel systems. All those algorithms are based on the backward reachability and suffered from complex computational consumption. Esparza et al. [29] introduced an incomplete but empirically efficient solution to the coverability problem. The new approach was based on classical Petri nets analysis techniques, the marking equation and traps [30, 31], and utilized an SMT solver to implement the constraint approach. Inspired by Esparza’s work, Athanasiou et al. [32] introduced an approximate coverability method by using thread state equations and implemented it in a tool named TSE. TSE is very capable on Boolean programs but theoretically incomplete.


## 3. Preliminaries

### 3.1. Nicely Sliceable WSTS

Definition 1 (well-quasi-ordering).
A well-quasi-ordering (wqo) is a reflexive and transitive binary relation⪯ over set X, and for every infinite sequence x0,x1,x2,… of elements from X, there exists i<j such that xi⪯xj.ForY⊆X, the upward-closure of Y is the set ↑Y={x∣∃y∈Y,y⪯x}. A basis of an upward-closed set Y is a set B⊆Y such that Y=↑B. A set U is said to be ⪯-upward-closed (or simply upward-closed if ⪯ is clear from the context) if U=↑U. It is known that if ⪯ is a wqo, then any ⪯ -upward-closed set has a unique finite basis B such that for all x,y∈B we have x⪯y and y⪯x [33]. Given upward-closed U, we let basis(U) denote the unique finite basis of U. Moreover, it is known that any infinite increasing sequence S0⊆S1⊆S2⊆⋯ of upward-closed sets eventually stabilizes; that is, there exists k∈N such that Sk=Sk+1=Sk+2=⋯.Definition 2 (discrete wqo).
A wqo is a discrete wqo (dwqo) overX if for all x∈X there exists k∈N such that for any sequence x0≺x1≺⋯≺xl=x, we have l≤k. The weight function w:X→N maps each x to the minimum such as k. For the ⪯-upward-closed set U, the base weight of U is bw(U)=max⁡{w(x)∣x∈basis(U)}.The weight functionw(x) slices the state space into a countable number of finite sets S0,S1,S2,…, where Si={x∈S∣w(x)=i}. This property allows for finite state model checking techniques to be used to the reachability for each weighted bounded Si.Definition 3 (nicely sliceable well-structured transition systems).
A nicely sliceable well-structured transition system (NSW)M=(S,→,⪯) is a transition system equipped with a dwqo on its states that satisfies the following properties:(1)
S is the (possibly infinite) state space.(2)
→⊆S×S is transition relation.(3)
⪯ is a dwqo over S.(4)
For allx,x′,y∈S, if x→x′ and x⪯y, there exists y′ such that y→y′ and x′⪯y′.(5)
Weight-respecting: for allx,x′,y∈S, w(x′)-w(x)=w(y′)-w(y).(6)
δ-deflatable: for δ∈N if whenever x→x′ and z⪯x′, there exists y and y′ such that the following properties hold: (1)  y⪯x, (2)  y→y′, (3)  z⪯y′, (4)  w(y)≤w(z)+δ, and (5)  w(y′)≤w(z)+δ.


### 3.2. Thread Transition Systems

Thread transition systems (TTS) are motivated by the verification task of multithread asynchronous programs, which is the subset of NSW. LetL and S be finite sets forlocal andshared states, respectively. The elements of T=S×L are calledthread states.Definition 4 (thread transition system).
A thread transition system (TTS) is a pairT,R, where R⊆T×T is a binary relation on T, partitioned into R=↦∪↪.LetV=⋃n=1∞(S×Ln). The elements of V are calledstates. We write them in the form (s∣l1,l2,…,ln). A TTS gives rise to a transition system M=(V,↣) with (1)s∣l1,l2,…,ln↣s′∣l1′,l2′,…,ln′′,if one of the following conditions holds.Thread Transitions. n′=n and there exists (s,l)↦(s′,l′)∈R and i such that li=l,  li′=l′, and, for all j≠i,  lj′=lj.Spawn Transitions. n′=n+1 and there exists (s,l)↪(s′,l′)∈R and i such that li=l,  ln′′=l′, and for all j<n′,  lj′=lj.LetIl⊆L be a set of initial local states and Is⊆S be a set of initial shared states. We define the set of initial states to be I=Is×⋃n=1∞Iln. An execution of the transition system M is a finite or infinite sequence of states in V whose adjacent states are related by ↣, which started at initial states. A state is reachable if it appears in some execution.In order to state the coverability problem, define thecover relation ⪯ over V as (s∣l1,l2,…,ln)⪯(s′∣l1′,l2′,…,ln′′) if s=s′ and [l1,ln,…,ln]⊆[l1′,l2′,…,ln′′], where [·] denotes amultiset.Give target statesvF∈V, if vF is coverable; that is, does there exists a path in M leading to a state v that covers vF: v⪰vF? The safety property is described as the upward-closed set of vF and converts into the coverability analysis problem.Acover relation ⪯ is neither symmetric nor antisymmetric, thus a quasi-order, and in fact a well-quasi-order (wqo) on V: any infinite sequence v1,v2,… of elements from V contains an increasing pair vi⪯vj with i<j. It is easy to see that (M,⪯) fulfills the definition of WSTS. A TTS with standard thread and spawn transition can be expressed as plain Petri nets [22] and is the subset class of NSW [20].


## 3.1. Nicely Sliceable WSTS

Definition 1 (well-quasi-ordering).
A well-quasi-ordering (wqo) is a reflexive and transitive binary relation⪯ over set X, and for every infinite sequence x0,x1,x2,… of elements from X, there exists i<j such that xi⪯xj.ForY⊆X, the upward-closure of Y is the set ↑Y={x∣∃y∈Y,y⪯x}. A basis of an upward-closed set Y is a set B⊆Y such that Y=↑B. A set U is said to be ⪯-upward-closed (or simply upward-closed if ⪯ is clear from the context) if U=↑U. It is known that if ⪯ is a wqo, then any ⪯ -upward-closed set has a unique finite basis B such that for all x,y∈B we have x⪯y and y⪯x [33]. Given upward-closed U, we let basis(U) denote the unique finite basis of U. Moreover, it is known that any infinite increasing sequence S0⊆S1⊆S2⊆⋯ of upward-closed sets eventually stabilizes; that is, there exists k∈N such that Sk=Sk+1=Sk+2=⋯.Definition 2 (discrete wqo).
A wqo is a discrete wqo (dwqo) overX if for all x∈X there exists k∈N such that for any sequence x0≺x1≺⋯≺xl=x, we have l≤k. The weight function w:X→N maps each x to the minimum such as k. For the ⪯-upward-closed set U, the base weight of U is bw(U)=max⁡{w(x)∣x∈basis(U)}.The weight functionw(x) slices the state space into a countable number of finite sets S0,S1,S2,…, where Si={x∈S∣w(x)=i}. This property allows for finite state model checking techniques to be used to the reachability for each weighted bounded Si.Definition 3 (nicely sliceable well-structured transition systems).
A nicely sliceable well-structured transition system (NSW)M=(S,→,⪯) is a transition system equipped with a dwqo on its states that satisfies the following properties:(1)
S is the (possibly infinite) state space.(2)
→⊆S×S is transition relation.(3)
⪯ is a dwqo over S.(4)
For allx,x′,y∈S, if x→x′ and x⪯y, there exists y′ such that y→y′ and x′⪯y′.(5)
Weight-respecting: for allx,x′,y∈S, w(x′)-w(x)=w(y′)-w(y).(6)
δ-deflatable: for δ∈N if whenever x→x′ and z⪯x′, there exists y and y′ such that the following properties hold: (1)  y⪯x, (2)  y→y′, (3)  z⪯y′, (4)  w(y)≤w(z)+δ, and (5)  w(y′)≤w(z)+δ.


## 3.2. Thread Transition Systems

Thread transition systems (TTS) are motivated by the verification task of multithread asynchronous programs, which is the subset of NSW. LetL and S be finite sets forlocal andshared states, respectively. The elements of T=S×L are calledthread states.Definition 4 (thread transition system).
A thread transition system (TTS) is a pairT,R, where R⊆T×T is a binary relation on T, partitioned into R=↦∪↪.LetV=⋃n=1∞(S×Ln). The elements of V are calledstates. We write them in the form (s∣l1,l2,…,ln). A TTS gives rise to a transition system M=(V,↣) with (1)s∣l1,l2,…,ln↣s′∣l1′,l2′,…,ln′′,if one of the following conditions holds.Thread Transitions. n′=n and there exists (s,l)↦(s′,l′)∈R and i such that li=l,  li′=l′, and, for all j≠i,  lj′=lj.Spawn Transitions. n′=n+1 and there exists (s,l)↪(s′,l′)∈R and i such that li=l,  ln′′=l′, and for all j<n′,  lj′=lj.LetIl⊆L be a set of initial local states and Is⊆S be a set of initial shared states. We define the set of initial states to be I=Is×⋃n=1∞Iln. An execution of the transition system M is a finite or infinite sequence of states in V whose adjacent states are related by ↣, which started at initial states. A state is reachable if it appears in some execution.In order to state the coverability problem, define thecover relation ⪯ over V as (s∣l1,l2,…,ln)⪯(s′∣l1′,l2′,…,ln′′) if s=s′ and [l1,ln,…,ln]⊆[l1′,l2′,…,ln′′], where [·] denotes amultiset.Give target statesvF∈V, if vF is coverable; that is, does there exists a path in M leading to a state v that covers vF: v⪰vF? The safety property is described as the upward-closed set of vF and converts into the coverability analysis problem.Acover relation ⪯ is neither symmetric nor antisymmetric, thus a quasi-order, and in fact a well-quasi-order (wqo) on V: any infinite sequence v1,v2,… of elements from V contains an increasing pair vi⪯vj with i<j. It is easy to see that (M,⪯) fulfills the definition of WSTS. A TTS with standard thread and spawn transition can be expressed as plain Petri nets [22] and is the subset class of NSW [20].


## 4. Multithreaded Programs Safety Verification

In this section, we introduce a new method for the safety verification of multithread programs. The input source code is translated into TTS by using SatAbs [34]. Then, we propose a novel TTS coverability analysis algorithm to verify the safety properties. Finally, the implementation details are described.


### 4.1. The Input Languages

Most popular programming languages such as Java and C/C++ embrace concurrent programming via theirpthread orthread class APIs, respectively. In this paper, we focus on the pthread-style multithreaded ANSI-C programs. ANSI-C is one of the most popular programming languages for safety critical embedded software. The mobile crowdsourcing networks contains most embedded devices which are based on multithreaded programs to support the crowdsourcing computing and communications. SatAbs is an SAT-based model checker by predicate abstraction, and can be used to model the ANSI-C programs into TTS format. We follow the introduction from the SatAbs website (http://www.cprover.org/satabs/) to transform the ANSI-C programs into TTS. All ANSI-C programs can be translated into Boolean programs by SatAbs, completely. The safety properties can be reserved during the formalization process.


### 4.2. IC3-Based Thread Transition System Coverability Analysis Algorithm

IC3 is SAT-based and computes inductive overapproximations of reachable sets. LetI and P be initial states and the property states, respectively. Also let T denote the transition relation over the current and the next states. IC3 maintains a trace: [R0,R1,…,RN]. The first element R0 is the initial states. For i>0,  Ri is a set of clauses that AND-ed together and represent an overapproximation of the states reachable from the initial states in k steps or less. Ri→Ri+1, and the clauses Ri+1 are a subset of Ri, except for i=0. The IC3 algorithm will terminate if a counterexample is found or an inductive proof RN is got.This section develops our new algorithm, TTSCov, which is based on the IC3 algorithm. For a target setvF and i∈N,  wl(vF,i) presents the set of weight limited vF by i. From the base weight of vF, the algorithm computes the overapproximation for the backward reachable set Oi. Oi is an inductive overapproximation of the states from vF which is reachable along a path that never exceeds weight i. We use IC3, an SAT-based finite state model checker, to compute this weight limited and inductive overapproximation of vF.As shown in Algorithm1, the input is a TTS M, a set of initial states I, and an ⪯-upward-closed set of target states vF. The variable i is the current weight boundary, which is initially the base weight of vF and increases by 1 each loop iteration. Oi is an overapproximation of br(vF,i), which initially is set as wl(vF,bw(vF)). Oi is an overapproximation of Oi-1 bounded by the weight i, which is computed by IC3 engine. If Oi intersected with the initial states I, the counterexample was found, and the algorithm terminated. In line (6), we check if Oi and Oi-1 are equal, if not, the variable n was assigned as the current i. If the condition of line (6) fails δ times consecutively, we have On+δ=On+δ-1=⋯=On, and thus the verification is successful.Algorithm 1:TTSCov.
Intput:
M=(S,→,⪯): a TTS model to describe a multi-threaded program
I⊆S: the inital states
δ: a constant which depend on the input model M
vF: the target states, which is described as an upward-closed set
Output:
safe or unsafe
(1)i≔bw(vF),  n≔i,  Oi-1≔wl(vF,i)   // initialization
(2)whilen≥i-δdo
(3)Oi≔IC3(Oi-1,I,i)
(4)ifOi∩I≠∅then
(5)   printCEX
(6)   RETURNunsafe
(7)end if
(8)IfOi≠Oi-1then
(9)n≔i
(10)end if
(11)i≔i+1
(12)end while
(13) RETURNsafeActually, the condition in line(8) can be replaced by Oi≡Oi-1, and the algorithm works well under the syntactically equal check. But the syntactic checking is more efficient, as the IC3 algorithm builds the frame incrementally, and the clause in Oi is the subset in Oi-1. In order to take this feature, a Boolean variable can be used to check if new clauses add to Oi when computing the overapproximation at line (3). This speeds up the algorithm much more.The main routine in Algorithm1 is the while-loop. For each loop, the IC3 engine computes the overapproximation by using the SAT solver. The algorithm terminates when it finds a counterexample at line (5) or proves safety at line (13).


### 4.3. Implementation

A TTS with thread and spawn transitions is expressive as a plain Petri net. Zhang et al. [35] introduced a method to cut off a Petri net into a finite state machine (FSM). Inspired by Zhang’s work, this section introduces the details of how to bound the TTS into FSM.The TTS Format. The input multithreaded programs model are encoded in the TTS format (http://www.cprover.org/bfc/). Eachshared orlocal is mapped to ashared/local variable. Just oneshared variable can be assigned to “1,” and alllocal variables could be assigned to arbitrary natural number. A transition is a thread transition or spawn transition, which described how the thread state changed.The FSM Format: AIGER. AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs) (http://fmv.jku.at/aiger/). AIGs are a good way to describe a FSM and can be translated into a propositional logic for a SAT solver. The bounded TTS is encoded as an AIG model, where eachshared andlocal state corresponds to state variables. Extra input variables are introduced to select which rule to be fired, and then update the state variables’ value to set up the transition relations equally.Shared and Local Variables. An S-bit vector was used to encode allshared variables, as just one shared variable was assigned with “1” at the same time. For eachlocal variable, the unary encoding was used to encode the natural numbers n, as literature [35] shows that one-hot encoding is one possible unary encoding. As shown in Table 1, thermometer encoding is another unary encoding and performs well when using the incremental SAT solvers. In this paper, thermometer encoding is used to encode thelocal variables.Table 1
Encoding: binary, one-hot, and thermometer.
n
Binary
One-hot
Thermometer
0
000
00000001
00000001
1
001
00000010
00000011
2
010
00000100
00000111
3
011
00001000
00001111
4
100
00010000
00011111
5
101
00100000
00111111
6
110
01000000
01111111
7
111
10000000
11111111A full adder is used to bound the total thread number, and the logic is the same as described in [35]. The total thread number is the sum of alllocal variables’ value. As the thermometer encoding technique is used to encode the local variables, the structure information is also added as the constraint to the AIG model.


## 4.1. The Input Languages

Most popular programming languages such as Java and C/C++ embrace concurrent programming via theirpthread orthread class APIs, respectively. In this paper, we focus on the pthread-style multithreaded ANSI-C programs. ANSI-C is one of the most popular programming languages for safety critical embedded software. The mobile crowdsourcing networks contains most embedded devices which are based on multithreaded programs to support the crowdsourcing computing and communications. SatAbs is an SAT-based model checker by predicate abstraction, and can be used to model the ANSI-C programs into TTS format. We follow the introduction from the SatAbs website (http://www.cprover.org/satabs/) to transform the ANSI-C programs into TTS. All ANSI-C programs can be translated into Boolean programs by SatAbs, completely. The safety properties can be reserved during the formalization process.


## 4.2. IC3-Based Thread Transition System Coverability Analysis Algorithm

IC3 is SAT-based and computes inductive overapproximations of reachable sets. LetI and P be initial states and the property states, respectively. Also let T denote the transition relation over the current and the next states. IC3 maintains a trace: [R0,R1,…,RN]. The first element R0 is the initial states. For i>0,  Ri is a set of clauses that AND-ed together and represent an overapproximation of the states reachable from the initial states in k steps or less. Ri→Ri+1, and the clauses Ri+1 are a subset of Ri, except for i=0. The IC3 algorithm will terminate if a counterexample is found or an inductive proof RN is got.This section develops our new algorithm, TTSCov, which is based on the IC3 algorithm. For a target setvF and i∈N,  wl(vF,i) presents the set of weight limited vF by i. From the base weight of vF, the algorithm computes the overapproximation for the backward reachable set Oi. Oi is an inductive overapproximation of the states from vF which is reachable along a path that never exceeds weight i. We use IC3, an SAT-based finite state model checker, to compute this weight limited and inductive overapproximation of vF.As shown in Algorithm1, the input is a TTS M, a set of initial states I, and an ⪯-upward-closed set of target states vF. The variable i is the current weight boundary, which is initially the base weight of vF and increases by 1 each loop iteration. Oi is an overapproximation of br(vF,i), which initially is set as wl(vF,bw(vF)). Oi is an overapproximation of Oi-1 bounded by the weight i, which is computed by IC3 engine. If Oi intersected with the initial states I, the counterexample was found, and the algorithm terminated. In line (6), we check if Oi and Oi-1 are equal, if not, the variable n was assigned as the current i. If the condition of line (6) fails δ times consecutively, we have On+δ=On+δ-1=⋯=On, and thus the verification is successful.Algorithm 1:TTSCov.
Intput:
M=(S,→,⪯): a TTS model to describe a multi-threaded program
I⊆S: the inital states
δ: a constant which depend on the input model M
vF: the target states, which is described as an upward-closed set
Output:
safe or unsafe
(1)i≔bw(vF),  n≔i,  Oi-1≔wl(vF,i)   // initialization
(2)whilen≥i-δdo
(3)Oi≔IC3(Oi-1,I,i)
(4)ifOi∩I≠∅then
(5)   printCEX
(6)   RETURNunsafe
(7)end if
(8)IfOi≠Oi-1then
(9)n≔i
(10)end if
(11)i≔i+1
(12)end while
(13) RETURNsafeActually, the condition in line(8) can be replaced by Oi≡Oi-1, and the algorithm works well under the syntactically equal check. But the syntactic checking is more efficient, as the IC3 algorithm builds the frame incrementally, and the clause in Oi is the subset in Oi-1. In order to take this feature, a Boolean variable can be used to check if new clauses add to Oi when computing the overapproximation at line (3). This speeds up the algorithm much more.The main routine in Algorithm1 is the while-loop. For each loop, the IC3 engine computes the overapproximation by using the SAT solver. The algorithm terminates when it finds a counterexample at line (5) or proves safety at line (13).


## 4.3. Implementation

A TTS with thread and spawn transitions is expressive as a plain Petri net. Zhang et al. [35] introduced a method to cut off a Petri net into a finite state machine (FSM). Inspired by Zhang’s work, this section introduces the details of how to bound the TTS into FSM.The TTS Format. The input multithreaded programs model are encoded in the TTS format (http://www.cprover.org/bfc/). Eachshared orlocal is mapped to ashared/local variable. Just oneshared variable can be assigned to “1,” and alllocal variables could be assigned to arbitrary natural number. A transition is a thread transition or spawn transition, which described how the thread state changed.The FSM Format: AIGER. AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs) (http://fmv.jku.at/aiger/). AIGs are a good way to describe a FSM and can be translated into a propositional logic for a SAT solver. The bounded TTS is encoded as an AIG model, where eachshared andlocal state corresponds to state variables. Extra input variables are introduced to select which rule to be fired, and then update the state variables’ value to set up the transition relations equally.Shared and Local Variables. An S-bit vector was used to encode allshared variables, as just one shared variable was assigned with “1” at the same time. For eachlocal variable, the unary encoding was used to encode the natural numbers n, as literature [35] shows that one-hot encoding is one possible unary encoding. As shown in Table 1, thermometer encoding is another unary encoding and performs well when using the incremental SAT solvers. In this paper, thermometer encoding is used to encode thelocal variables.Table 1
Encoding: binary, one-hot, and thermometer.
n
Binary
One-hot
Thermometer
0
000
00000001
00000001
1
001
00000010
00000011
2
010
00000100
00000111
3
011
00001000
00001111
4
100
00010000
00011111
5
101
00100000
00111111
6
110
01000000
01111111
7
111
10000000
11111111A full adder is used to bound the total thread number, and the logic is the same as described in [35]. The total thread number is the sum of alllocal variables’ value. As the thermometer encoding technique is used to encode the local variables, the structure information is also added as the constraint to the AIG model.


## 5. Experimental Evaluation

We have implemented our algorithm in a tool named TTSCov. TTSCov is implemented with C++, and all input instances are encoded in TTS format. Petri nets tools are used by converting TTS instances into MIST format (https://github.com/pierreganty/mist). Most crowdsourcing programs are described in pthread-style multithreaded ANSI-C. SatAbs is the front-end of TTSCov, which translates the input ANSI-C programs in to TTS.To measure TTSCov’s performance, we compare with the state-of-the-art tools: MIST, IIC [21], BFC [11], Petrinizer [29], and TSE [32]. All experiments are performed on an Intel 3.4 GHz Intel, and 16 GB of memory, running Linux OS in 64-bit. The CPU time is limited to 1 hour, and memory to 10 GB.


### 5.1. Benchmarks

We collect 178 Petri nets examples from the Petrinizer repository (https://github.com/cryptica/pnerf), in which 115 instances are safe and 63 instances are unsafe. All examples are organized into five suites. The first suite is a collection of plain Petri nets from the MIST toolkit. This suit contains 23 Petri nets (17 instances are safe, and the rest are unsafe) and 6 bounded Petri nets which are all safe. The second suite comes from the provenance analysis of message in a medical system, which contains 12 safe instances. The third suite also comes from the provenance analysis of message in bug tracking application, which contains 40 safe instances and 1 unsafe instance. The fourth suite contains 46 instances that are used to evaluate the BFC tool(http://www.cprover.org/bfc). Those instances are generated from concurrent C program in TTS format. They are mostly unsafe, and just 2 instances are safe. The fifth suite contains 50 instances that comes from the Erlang verification tool called Soter [36], and those examples can be found on Soter’s Website (http://mjolnir.cs.ox.ac.uk/soter). Out of 50 instances in this suite, 38 are safe. This suite contains the largest example in the collection, with 66,950 places and 213,635 transitions.


### 5.2. Rate of Success on All Instances

We run two different version of BFC, named BFC v1.0 and BFC v2.0, respectively. The BFC tool has 3 modes: backward, forward, and concurrent. In concurrent mode, two threads are used to run backward and forward parallel. But we find there is a potential bug in BFC v2.0 with concurrent mode. The tool got stuck in concurrent mode when switching the thread. We run 10 times in concurrent mode and show the median results in Figure1. Petrinizer is an SMT-based tool, which has 8 parameters, and the tool may return wrong answer for some examples. If Petrinizer returns wrong result in one configuration, we say the result is wrong. All five algorithms in MIST toolkit were compared.Figure 1
Total instances. All 178 instances are separated into safe and unsafe by the real results. There are 115 safe instances, and 63 unsafe instances. TTSCov compare with the state-of-the-art tools: MIST, IIC, BFC, Petrinizer, and TSE. There are two versions of BFC tool, and for each version, the tool has three modes.BFC2c means the BFC v2.0 run in concurrent mode. f and b respect forward and backward, respectively. MIST toolkit implemented five algorithms: Backward, EEC, TSI, IC4PN, and CEGAR.Figure1 shows that TTSCov performs better than the other complete tools, which solve 147 instances in total the same as Petrinizer, which is incomplete. For safe instances, TTSCov solves 91 out of 115, and 22 instances timeout. Most importantly, there are just 2 instances over the memory limit, which support the IC3 less memory usage. Petrinzier solves 84 instances, and 1 timeout. But 30 instances return unsafe results for those safe instances. Out of 30 wrong results examples, 19 instances return wrong answer with all 8 configurations, and the others are partly wrong. TSE solves 84 instances, 10 out of memory and 21 timeout. BFC2c solves 67 examples in total, whereas 30 examples time out and 18 instances are out of memory. BFC2b performs same as BFC2c, in which 66 instances are solved, but with more out of time instances. BFC1c solves 53 out of 115 safe instances, and 61 examples out of memory limit, with just one timeout. BFC1b solves 47 safe instances, and 9 out of time limit and 59 out of memory limit. The forward algorithm performs worst in both BFC v1.0 and BFC v2.0, where 34 instances and 35 instances are solved by BFC2f and BFC1f, respectively. There are 53 instances of timeout for both tools. The BFC2f has 28 examples out of memory, and the BFC1f runs out of memory limit for 27 examples. IIC solves 47 instances, 24 instances timeout and 44 instances out of memory. For five algorithms in MIST toolkit, EEC solves 56 instances, 13 instances timeout, and 46 out of memory. Backward algorithm performs the same as EEC, 5 more instances timeout. TSI and IC4PN solve about 30 safe instances, but CEGAR just solves 8.For unsafe instances, TTSCov solves 56 examples out of 63, no out of memory case, but 7 timeout. Petrinizer and BFC perform well in those suite cases. Petrinizer,BFC1c, and BFC1f solve all 63 unsafe instances. TSE solves 62 instances, and just one out of memory. BFC1b has 4 timeout and 4 out of memory, respectively. BFC2b has 8 instances out of time or memory limitation, and BFC2f just has 2 instances out of memory. BFC2c performs worse, where 30 instances are solved, because of the potential bugs in concurrent mode. For some unsafe instances in the fourth suite, the forward thread has found the counterexample, but got stuck when switching the thread until timeout. What is more, there are 3 examples out of memory when running BFC v2.0 in concurrent mode. IIC and Backward performs almost the same, which solve about 50 instances, 1 out of memory and the rest are timeout. EEC, TSI, IC4PN, and CEGAR are not good on unsafe instances, especially CEGAR, which only solves 2 unsafe instances.In brief, TTSCov performs well both for safe and unsafe instances, especially in memory usage. Petrinizer performs well in time and memory usage for all instances, but reports wrong answer for safe instances. TSE performs nearly the same as TTSCov, but incomplete the same as Petrinizer. BFC v1.0 and v2.0 are good at unsafe cases, excluding the potential bugs inBFC2c. IIC and MIST perform the same, but take more memory usage.


### 5.3. Tools Combination

Petrinizer and TSE are incomplete, but perform excellently on time and memory usage. We combine the Petrinizer and TSE with the other tools, and the total solved instances number is shown in Table2.Table 2
Petrinizer and TSE combine with the other tools. For each suite, we focus on the instance that Petrinizer or TSE are unsolved, but the combined tool is solved, then present the total number of solved instances. All data are under taking the sum of the instances that Petrinizer or TSE can solve and the disjoint instances that the other tools can solve.
Petri (29)
Medical (12)
Bug-tr (41)
Wa-kr (46)
Soter (50)
Total (178)
Petrinizer
21
4
33
46
43
147
Petrinizer + MIST
29
12
33
46
47
167
Petrinizer + BFC
27
4
33
46
49
159
Petrinizer + IIC
29
9
33
46
47
164
Petrinizer + TTSCov
29
12
41
46
49
177
TSE
19
4
33
46
44
146
TSE + MIST
29
12
33
46
47
167
TSE + BFC
27
4
33
46
49
159
TSE + IIC
29
9
33
46
47
164
TSE + TTSCov
29
12
41
46
49
177Petrinizer works out 147 instances alone, but 30 instances return wrong or partly wrong result. For BFC, we compared the BFC v1.0 and BFC v2.0 in all three modes and then chose the best one. MIST stands forBackward algorithm, which performs the best of five algorithms in the MIST toolkit. When combining BFC with Petrinizer, 159 instances are solved. IIC and MIST solve 164 and 167, respectively, when working together with Petrinizer. Our tool TTSCov can solve 177 instances when combined with Petrinizer.TSE solves 146 instances in total. When combined with the other tools, the total solved instances number is the same as Petrinizer. More importantly, TTSCov can solve all collected instances when combined with Petrinizer or TSE, except one instance from the Soter suite, which all tools can not deal with.


### 5.4. Memory Usage Evaluation

To show the memory usage of TTSCov, we compare with MIST, IIC, and BFC. Figure2 shows that TTSCov is an efficient tool in memory usage, due to the use of IC3 as the back-end engine. TTSCov solves nearly 97.3% instances within 1 GB memory. About two-thirds instances can be solved within 2 GB for all tools, but TTSCov and BFC perform better than MIST and IIC in large instances. We find a bug when running BFC v2.0 for some instances from the forth instance suite. The tool has a segmentation fault for two instances, and we have get the bug confirmation from the author. The segmentation fault instances are marked as out of memory. Petrinizer and TSE are indeed efficient for memory usage, but incomplete. Therefore, we do not compare with those. TTSCov is based on the IC3 engine, which solves the verification problem without unrolling the transition relations. This is the main reason for why TTSCov performs well in memory usage. In conclusion, TTSCov is an efficient tool in memory usage, especially for huge instances.Figure 2
Comparison of TTSCov with MIST, IIC, and BFC for memory usage. BFC stands forBFC2b. We use two versions BFC in all three modes and find that the BFC2b performs the best in memory usage test. Backward algorithm is the best of five algorithms for memory usage in MIST toolkit, so MIST represented the Backward algorithm. For all timeout instances, we also show the memory usage in this figure.


## 5.1. Benchmarks

We collect 178 Petri nets examples from the Petrinizer repository (https://github.com/cryptica/pnerf), in which 115 instances are safe and 63 instances are unsafe. All examples are organized into five suites. The first suite is a collection of plain Petri nets from the MIST toolkit. This suit contains 23 Petri nets (17 instances are safe, and the rest are unsafe) and 6 bounded Petri nets which are all safe. The second suite comes from the provenance analysis of message in a medical system, which contains 12 safe instances. The third suite also comes from the provenance analysis of message in bug tracking application, which contains 40 safe instances and 1 unsafe instance. The fourth suite contains 46 instances that are used to evaluate the BFC tool(http://www.cprover.org/bfc). Those instances are generated from concurrent C program in TTS format. They are mostly unsafe, and just 2 instances are safe. The fifth suite contains 50 instances that comes from the Erlang verification tool called Soter [36], and those examples can be found on Soter’s Website (http://mjolnir.cs.ox.ac.uk/soter). Out of 50 instances in this suite, 38 are safe. This suite contains the largest example in the collection, with 66,950 places and 213,635 transitions.


## 5.2. Rate of Success on All Instances

We run two different version of BFC, named BFC v1.0 and BFC v2.0, respectively. The BFC tool has 3 modes: backward, forward, and concurrent. In concurrent mode, two threads are used to run backward and forward parallel. But we find there is a potential bug in BFC v2.0 with concurrent mode. The tool got stuck in concurrent mode when switching the thread. We run 10 times in concurrent mode and show the median results in Figure1. Petrinizer is an SMT-based tool, which has 8 parameters, and the tool may return wrong answer for some examples. If Petrinizer returns wrong result in one configuration, we say the result is wrong. All five algorithms in MIST toolkit were compared.Figure 1
Total instances. All 178 instances are separated into safe and unsafe by the real results. There are 115 safe instances, and 63 unsafe instances. TTSCov compare with the state-of-the-art tools: MIST, IIC, BFC, Petrinizer, and TSE. There are two versions of BFC tool, and for each version, the tool has three modes.BFC2c means the BFC v2.0 run in concurrent mode. f and b respect forward and backward, respectively. MIST toolkit implemented five algorithms: Backward, EEC, TSI, IC4PN, and CEGAR.Figure1 shows that TTSCov performs better than the other complete tools, which solve 147 instances in total the same as Petrinizer, which is incomplete. For safe instances, TTSCov solves 91 out of 115, and 22 instances timeout. Most importantly, there are just 2 instances over the memory limit, which support the IC3 less memory usage. Petrinzier solves 84 instances, and 1 timeout. But 30 instances return unsafe results for those safe instances. Out of 30 wrong results examples, 19 instances return wrong answer with all 8 configurations, and the others are partly wrong. TSE solves 84 instances, 10 out of memory and 21 timeout. BFC2c solves 67 examples in total, whereas 30 examples time out and 18 instances are out of memory. BFC2b performs same as BFC2c, in which 66 instances are solved, but with more out of time instances. BFC1c solves 53 out of 115 safe instances, and 61 examples out of memory limit, with just one timeout. BFC1b solves 47 safe instances, and 9 out of time limit and 59 out of memory limit. The forward algorithm performs worst in both BFC v1.0 and BFC v2.0, where 34 instances and 35 instances are solved by BFC2f and BFC1f, respectively. There are 53 instances of timeout for both tools. The BFC2f has 28 examples out of memory, and the BFC1f runs out of memory limit for 27 examples. IIC solves 47 instances, 24 instances timeout and 44 instances out of memory. For five algorithms in MIST toolkit, EEC solves 56 instances, 13 instances timeout, and 46 out of memory. Backward algorithm performs the same as EEC, 5 more instances timeout. TSI and IC4PN solve about 30 safe instances, but CEGAR just solves 8.For unsafe instances, TTSCov solves 56 examples out of 63, no out of memory case, but 7 timeout. Petrinizer and BFC perform well in those suite cases. Petrinizer,BFC1c, and BFC1f solve all 63 unsafe instances. TSE solves 62 instances, and just one out of memory. BFC1b has 4 timeout and 4 out of memory, respectively. BFC2b has 8 instances out of time or memory limitation, and BFC2f just has 2 instances out of memory. BFC2c performs worse, where 30 instances are solved, because of the potential bugs in concurrent mode. For some unsafe instances in the fourth suite, the forward thread has found the counterexample, but got stuck when switching the thread until timeout. What is more, there are 3 examples out of memory when running BFC v2.0 in concurrent mode. IIC and Backward performs almost the same, which solve about 50 instances, 1 out of memory and the rest are timeout. EEC, TSI, IC4PN, and CEGAR are not good on unsafe instances, especially CEGAR, which only solves 2 unsafe instances.In brief, TTSCov performs well both for safe and unsafe instances, especially in memory usage. Petrinizer performs well in time and memory usage for all instances, but reports wrong answer for safe instances. TSE performs nearly the same as TTSCov, but incomplete the same as Petrinizer. BFC v1.0 and v2.0 are good at unsafe cases, excluding the potential bugs inBFC2c. IIC and MIST perform the same, but take more memory usage.


## 5.3. Tools Combination

Petrinizer and TSE are incomplete, but perform excellently on time and memory usage. We combine the Petrinizer and TSE with the other tools, and the total solved instances number is shown in Table2.Table 2
Petrinizer and TSE combine with the other tools. For each suite, we focus on the instance that Petrinizer or TSE are unsolved, but the combined tool is solved, then present the total number of solved instances. All data are under taking the sum of the instances that Petrinizer or TSE can solve and the disjoint instances that the other tools can solve.
Petri (29)
Medical (12)
Bug-tr (41)
Wa-kr (46)
Soter (50)
Total (178)
Petrinizer
21
4
33
46
43
147
Petrinizer + MIST
29
12
33
46
47
167
Petrinizer + BFC
27
4
33
46
49
159
Petrinizer + IIC
29
9
33
46
47
164
Petrinizer + TTSCov
29
12
41
46
49
177
TSE
19
4
33
46
44
146
TSE + MIST
29
12
33
46
47
167
TSE + BFC
27
4
33
46
49
159
TSE + IIC
29
9
33
46
47
164
TSE + TTSCov
29
12
41
46
49
177Petrinizer works out 147 instances alone, but 30 instances return wrong or partly wrong result. For BFC, we compared the BFC v1.0 and BFC v2.0 in all three modes and then chose the best one. MIST stands forBackward algorithm, which performs the best of five algorithms in the MIST toolkit. When combining BFC with Petrinizer, 159 instances are solved. IIC and MIST solve 164 and 167, respectively, when working together with Petrinizer. Our tool TTSCov can solve 177 instances when combined with Petrinizer.TSE solves 146 instances in total. When combined with the other tools, the total solved instances number is the same as Petrinizer. More importantly, TTSCov can solve all collected instances when combined with Petrinizer or TSE, except one instance from the Soter suite, which all tools can not deal with.


## 5.4. Memory Usage Evaluation

To show the memory usage of TTSCov, we compare with MIST, IIC, and BFC. Figure2 shows that TTSCov is an efficient tool in memory usage, due to the use of IC3 as the back-end engine. TTSCov solves nearly 97.3% instances within 1 GB memory. About two-thirds instances can be solved within 2 GB for all tools, but TTSCov and BFC perform better than MIST and IIC in large instances. We find a bug when running BFC v2.0 for some instances from the forth instance suite. The tool has a segmentation fault for two instances, and we have get the bug confirmation from the author. The segmentation fault instances are marked as out of memory. Petrinizer and TSE are indeed efficient for memory usage, but incomplete. Therefore, we do not compare with those. TTSCov is based on the IC3 engine, which solves the verification problem without unrolling the transition relations. This is the main reason for why TTSCov performs well in memory usage. In conclusion, TTSCov is an efficient tool in memory usage, especially for huge instances.Figure 2
Comparison of TTSCov with MIST, IIC, and BFC for memory usage. BFC stands forBFC2b. We use two versions BFC in all three modes and find that the BFC2b performs the best in memory usage test. Backward algorithm is the best of five algorithms for memory usage in MIST toolkit, so MIST represented the Backward algorithm. For all timeout instances, we also show the memory usage in this figure.


## 6. Conclusion and Future Works

This paper introduce an IC3-based algorithm to verify the safety properties of multithreaded programs in mobile crowdsourcing networks. The pthread-style multithreaded program is modeled as a TTS. Then the state-of-the-art SAT-based model checking algorithm is used to verify the safety properties, by computing a series of overapproximation reachability with IC3. The results show that our new approach can solve more instances compared favorably against several recently published approaches. Due to using IC3 as the back-end engine, our method is significant for its lower memory consumption. Tools combination is a good direction to solve the multithreaded programs for more complex mobile crowdsourcing networks. Parallel programming will be a good way to speed up the TTSCov algorithm.



---

*Source: 3193974-2018-01-28.xml*