Verification and Testing

Question 1

Soundness

Answer 1

No incorrect programs are deemed correct ( ⇒ All errors are found)

Question 2

Completeness

Answer 2

A correct program is deemed correct ( ⇒ no spurious errors)

Question 3

Static verification

Answer 3

Consider program code, check
for all possible executions

Question 4

Dynamic verification

Answer 4

Runtime verification of executions

Question 5

Deadlocks

Answer 5

A deadlock is a circular wait

show themselves when a program hangs

hard to find because they often occur only with a specific scheduling

hard to reproduce

Question 6

Race conditions

Answer 6

two or more threads can access shared data and they try to change it at the same time

If the result of an execution depends on the execution order of two threads, one says that there is a race condition

Question 7

data race

Answer 7

1. Two threads access variable concurrently
2. At least one access is write
3. Nothing prevents simultaneous access

Question 8

gate lock

Answer 8

A gate lock prevents a deadlock by protecting the areas with lock reversal

Question 9

Lock Tree Algorithm

Answer 9

Dynamic algorithm to find deadlocks

in a tree, keep track the order in which locks are
acquired and released; see if there are reversals

Limitations
• Works for deadlocks involving two threads only
• Works only for properly nested locks

T1
ALock
BLock
T2
BLock
ALock

Question 10

Lock Tree Algorithm - steps

Answer 10

Build trees during runtime
– each tree has a current node
– If lock acquired create new child and move to it
– If node released, move up one level

After termination, analyze trees. Possible deadlock if

1. T1 contains a node Li with ancestor Lj
2. T2 tree contains a node Lj with ancestor Li
3. There is no gate lock: node Lk which is an ancestor of Li in T1 and Lj in T2

A gate lock is a lock that is

1. an ancestor of Li and Lj in T1 and
2. an ancestor of Li and Lj in T2

Question 11

Eraser

Answer 11

finds possible race conditions

Check locking behavior
For any shared data, is some lock always held on
access?
This condition is sufficient but not necessary for
correctness
Dynamic algorithm
– Computes locks held during one run
– May not find all problems
– May warn when no problem exists
– What it finds depends on the run!

Question 12

Why is eraser better at finding race conditions than simple testing?

Answer 12

Little dependence on scheduling order: Can find bug in
one scheduling by executing another one: better
than testing.

Question 13

Read-write locks

Answer 13

• multiple simultaneous readers,
• a write is never simultaneous with another read or write

Question 14

Valgrind

Answer 14

suite of tools, adds shadow memory

V-bits: One byte to store whether each bit has a valid value

A-bit: One bit to store whether byte has been allocated

Question 15

Purify

Answer 15

simpler version of valgrind

uses two bits of status per byte of memory

faster than valgrind, becaue only one bit per byte

Question 16

Logical gate symbols

Answer 16

Question 17

B(ounded)MC vs Concolic testing

Answer 17

BoundedMC tries all paths simultaneously
▪ Query: there is a path of length k to a bug
▪ Like breadth-first search: wide and shallow

Concolic tries one path at a time
▪ Query: this path (of length k) leads to a bug
▪ Like depth-first search: deep and narrow

Question 18

Java Path finder BFS vs DFS

Answer 18

BFS
•Finds shortest path to error
•Does not get stuck in infinite loop
•Typically uses more memory

DFS
•May not find error at all
•Often uses less memory

Question 19

Hoare triple

Answer 19

{P} S {Q}
P is the precondition
Q is the postcondition
S is a program
Meaning: if P holds before execution and S finishes, then Q holds afterwards.
Note: we prove partial correctness. If S runs forever, {P}S{Q} holds.

Question 20

Hoare Axioms

Answer 20