CpSc 513 Formal Verification Jan. 2, 2013
(officially "Integrated Systems Design")
0. Topics for today
* Course Overview
* Administrative stuff (grades, etc.)
I. Course Overview
A. What is Formal Verification?
Mathematically proving that a "design" has certain desired properties.
1. The design can be:
a. hardware: digital or analog
b. software: sequential, concurrent, distributed, ...
c. an embedded system: airplane, robot, wheelchair,
medical equipment
2. "mathematically proving" means we have:
a. a mathematically precise description of the design
b. a mathematically precise description of the desired properties
c. a valid proof.
3. proofs are hard
a. So, we look for classes of problems where the proofs can
be constructed automatically.
b. This creates lots of trade-offs between
amount of detail in the system model
amount of manual intervention required in the verification process
what properties we try to verify
B. What kinds of properties do we want to verify?
1. Equivalence: ForAll x. f(x) == g(x)
a. Used to compare "high-level" description with more detailed
implementation.
b. Example: database join
High level:
result = EmptySet;
forall t1 in R1 do
forall t2 in R2 do
if(field(i1, t1) == field(i2, t2))
result = result UNION { (t1, t2) }
end % if
end % for t2
end % for t1
Low-level -- lots of optimizations, depending on:
types of t1 and t2
index fields of R1 and R2
size of R1 and R2
"skew" in the relations
"skew" in the relations
memory hierarchy considerations
parallel/distributed implementations
c. Example: logic circuit equivalence
High level: register-transfer-level (RTL) description
RTL uses a programming language notation to give
expressions for the value loaded into each register
(i.e. flip-flop) on each clock cycle.
These expressions are implemented by networks of logic
gates.
Does the network of logic gates compute the same thing
as the RTL program?
2. Safety properties
a. A program never reaches a "bad" state.
b. We've now added the idea of time to our logic
* A program execution is a sequence of states.
* This sequence might be inifinitely long.
* A safety property says that all states satisfy some property.
c. Examples
* Never attempt a divide-by-zero, array-bounds violation,
null pointer dereference, invalud type cast, etc.
* Mutual exclusion: multiple threads can't attempt to access
some data structure at the same time.
* Deadlock freedom: the program never reaches a state where
there is a cycle of threads/processes waiting for each
other.
d. Safety properties have finite-length counterexamples.
3. Liveness properties
a. A program *eventually* reaches a good state
b. Examples:
* For sequential programs:
function calls eventually return,
the program eventually terminates,
etc.
* For reactive programs:
every request eventually gets a response
* For concurrent/parallel programs:
every thread/process waiting to enter a critical
region eventually manages to do so.
c. Liveness properties have infinite-length counterexamples.
* This makes reasoning about liveness properties more complicated.
* From an asymptotic complexity viewpoint, it tends to add an
extra exponential (or more) to the complexity.
* Requires reasoning about "fairness"
+ you might lose sometimes, but you can't lose all the time.
+ mathematically:
if p occurs infinitely often in execution X,
then q must occur infinitely often as well.
"p occurs infinitely often" means there is no state after
which no subsequent state satisifies p.
4. Refinement (aka "simulation" or "bisimulation"):
a. Let H be a program written at a high level of abstraction,
and L be a program written at a low level of abstraction.
b. Are H and L equivalent?
Does L preserve all safety properties of H?
Does L preserve all liveness properties of H?
C. How can we verify them?
1. The math
a. Safety properties
* Let P be a program
+ We can make a mathematical model for P where P is a function
(or relation) from states to states.
+ I won't worry about the details of what a "state" is right now,
but you can think of it as including:
- The values of variables that appear in the program.
- The values of local variables for every function currently
on the call-stack.
- The value of the program counter.
+ Let G: State -> boolean be the safety property that we want
to show.
+ Let Q0 be the set of possible initial states of P.
* Model-checking
+ The algorithm
Q_new = Q0;
Q = EmptySet;
repeat
Q = Q UNION Q_new;
Q_new = {q' | q' is reachable from q in one step of P} - Q;
until(Q_new == EmptySet);
+ Computable if the set of states of P is finite.
+ But, the state space can be huge, we may run out of time
or memory.
* Using invariants
+ Let I: State -> boolean
+ I is an invariant of P iff
ForAll (q, q') such that
q' is reachable from q in one step of P:
+ G is a safety property there is an invariant I such that
(Q0 => I) AND (I => G)
+ Proof: by induction
+ The hard part is finding I.
- Showing that I is an invariant, Q0 => I, and I => G
is "easy".
b. Liveness properties
+ We need "ranking functions"
+ Can be verified by model-checking but involves nested
fixpoints and even more (as in exponentially more) time.
+ Liveness is hard. That's enough for today.
2. The software
a. Symbolic computation
+ binary decision diagrams (BDDs):
- an "old" way to represent boolean expressions symbolically
- doesn't scale to large problems as well as modern SAT solvers
- but BDDs are very flexible; so we'll use them for examples.
+ SAT solvers
- turn any boolean satisfiability problem into 3-SAT
- solve or refute by case-splitting and backtracking
- the tricky part is finding good case splits and making use
of what the algorithm has learned from dead-ends when
backtracking.
+ Satisfiabiity-Modulo-Theories (SMT) solvers
- Start with a SAT solver
- Add decision procedures for
linear inequalities, non-linear arithmetic,
strings, lists, etc.
- And get a decision procedure for the combined theory.
- The elegant part is communicating useful information between
the different specialized solvers.
b. Model-checkers
+ Given a program, compute all reachable states to verify
safety properties.
+ Can also be used to verify liveness properties.
+ Works best with finite state spaces, but there are
generalizations that work for some special cases of
infinite state spaces.
c. Other reachability tools, etc.
D. Some more handy concepts
1. Non-determinism
a. Sometimes it's very helpful to leave some details of a program's
behaviour unspecified
+ Example: grocery shopping.
- I want to program my robot to go to the grocery store
and buy 1 litre of milk, 3 apples, and a loaf of bread.
- Does it matter what in what order the robot gets these
items from the grocery store shelves?
- Does it matter what exact path the robot takes in the store?
- Does it matter what variety of apple, or which brand of milk
or bread?
- I may want to leave these unspecified so that implementation
can choose (and perhaps optimize).
+ Example: mutual exclusion
- Alice and Bob each click on "Add to Cart" to get a copy of
"A Brief History of Fungus"
- Amazon only has one copy in stock.
- The server at amazon needs to process one "click" and then
reject that other, but it doesn't matter who gets the
book and who gets the out-of-stock notice.
- We can use non-determinism here.
b. Non-determinism can also be used to model the environment
of a program
+ The environment is *allowed* to do any of many possible choices.
+ The exact actions of the enivronment aren't specified.
c. Connection with non-determinism from automata theory
+ Automata theory:
A string s is in language L if there exists any set of
choices for the non-determinism that get it accepted.
+ Safety properties:
A program P fails to satisfy safety property S if there
exists any set of choices for the non-determinism that
leeds to a violating state.
+ Connection:
- Define a formal language tha recognizes the *failures* of S.
- Now, show that the language is empty.
d. Non-determinism is not randomness.
+ An implementation might always make the same choice.
For example, our grocery shopping robot might always
buy the items in alphabetical order.
+ An adversay can choose a very non-random order to cause a failure.
2. Abstraction
a. Let's say we have programs P and P' where P' is a "simpler"
version of P. In general, we mean that the set of states for
P' is (much) smaller than the set of states for P.
b. If every state transitino of P has a corresponding transition in
P', we say that P' is an abstraction of P.
c. An important consequence is that for every safety property we
can show for P', there is a corresponding safetry property
for P.
c. This lets us do our model-checking on a simpler program and
can make the model checking problem tractable. Note that P
may have safety properties that are "lost" by the abstraction
to P'. Thus, this method can produce "false negatives".
3. State explosion
a. In general, the number of states grows exponentially with the
number of state variables.
* The number of state variables typically grows linearly with the
length of the program text.
* Thus, the number of states grows exponentially with program size.
* This is called the state explosion problem.
b. A consequence is that brute-force methods for verification will
only work for small programs.
c. This motivates using abstraction, symbolic methods and other
techniques that we'll examine to get useful results for
real hardware and software designs.
E. What about intractability and undecidability?
1. Formal verification often involves problems that are NP-complete,
P-SPACE complete, undecidable, etc.
2. Just because a general class of problems is hard (or impossible)
does not mean that all specific instances are hard.
a. Does the following program halt?
public static void main(String[] args) {
System.out.println("hello world?"
}
b. How about this one:
public static void main(String[] args) {
for(int i = 0; i < 100; i = (i+1) % 100) {
System.out.println("this program never halts");
}
}
c. If the thalting problem is undecidable, how did you figure
out these two?
3. Formal methods researcher have developed methods that work
remarkably well for many practical problems.
a. In this course you'll learn about these methods.
b. You'll learn about places where "intractable" or "undecidable"
doesn't mean "give up".
c. You'll learn some aspects of complexity theory, and see how
complexity theory has connections to practical problems.
F. Who cares?
1. Hardware
a. Early applications:
equivalence checking show that an optimized logic circuit
has the same behaviour as a simple (but slower, bigger, etc.)
version of the "same" function.
b. Growing-up:
Verification of cache-coherence protocols.
Verification of arithmetic operations, esp. floating point.
c. Current areas:
Verifying many properties of state machines.
Checking large functional units: memory, arithmetic
instruction scheduling, etc.
2. Software
a. Early applications
Network protocol verification
"Extended static checks" (e.g. array bounds violations,
allocate/free errors, etc.).
b. Current work
Verifying properties of low-levels system code:
Low-level code can be modeled usefully using
finite-state-machines
Tedious and prone to errors
Errors are costly (can crash entire system, not just one
applications).
Verifying concurrent/parallel software
Informal reasoning-by-example often misses errors.
Assertional methods seem to be essential.
Security, embedded controllers, ...
G. Will I survive this course?
1. Yes
2. Formal verification spans many areas of computer science/engineering
a. This course will include:
i. Theory/math:
formal logic, complexity theory, differential equations,
temporal logic
ii. Systems:
examples from:
verifying standard algorithms
concurrent/parallel programming
computer architecture:
caches, arithmetic units, instruction execution
iii. Embedded systems and robotics
b. I'll include tutorials as needed.
* I will be very happy if you ask for a tutorial on some topic
3. The goal of the course is to have fun exploring how formal methods
have pratical values.
II. Administrative stuff
A. Finding your way around
1. The prof
a. Mark Greenstreet
b. mrg@cs.ubc.ca
c. ICICS/CS 323
d. Given the size of the class, I haven't planned for a formal
office hour.
* Just send me e-mail to make an appointment.
* If there's a demand for regular office hours, let me know,
in which case, I'll probablly propose Fridays, from 11am-12:30pm
2. The web
a. The course is on the web at
www.cs.ubc.ca/~mrg/cs513
b. I'll use piazza for on-line discussions
* www.piazza.com
* You can sign-up now
* After I announce this in class, I'll sign-up everyone from
registered according to the UBC registrar's office.
* I might link lecture notes, homework assignments, etc., to
the piazza page; or I might consider doing it once
(for www.cs.ubc.ca/~mrg/cs513) to be enough.
B. Grading, etc.
1. Homework -- I hope to have four homework assignments:
a. Using OBDDs (symbolic boolean expressions)
b. Model checking.
c. The Z3 SMT solver
d. Something with interval arithmetic solvers and/or
reachability tools for hybrid systems.
2. Projects
a. See http://www.cs.ubc.ca/~mrg/cs513/2012-2/project.html
* I'll add more to this later.
* A project should take ~40 hours of your time.
* I prefer individual projects but will consider a proposal for
a group project if:
+ A clear reason is given for why the project should be done
as a group project and not 2 more separate projects.
+ Clear criteria are given for evaluating each member's
contribution to the project.
b. Criteria
* < 80: you didn't do what you proposed, and you didn't provide
an acceptable redefinition of the project if you
hit some unforeseen difficulty (you can ask to
revise your project proposal if you hit problems).
* 80..84: you did what you proposed, but it's not clear that you
learned anything new in the process.
* 85..89: you learned something by doing the project. In other
words, for the topic of the project, you went beyond
what we've coverd in the course and found something
new.
* 90.. 94: I learned something by reading your report.
* 95..100: The work is worthy of writing a paper that I expect
to be a landmark in the field.
3. Class participation
a. For 12 of the papers covered in the course you need to write
a short summary that addresses the following questions:
i. What problem does the paper address?
ii. What is the key insight/idea in the paper's solution to this
problem?
iii. What did the authors implement/prove/etc. to demonstrate
their idea?
iv. How does their implemention/proof/etc validate their main
claims?
v. What are your questions or comments on the paper?
b. For each of these questions, you should write a 2-5 sentence
response.
c. Your class participation grade will be
(#summaries written)/12 * (average grade of summaries written)
4. Grading formula (may change depending on how many homework
assignments actually happen, etc.):
0.5*max(HW, Project) + 0.4*min(HW, Project) + 0.1*Participation
5. Collaboration policy
a. I encourage collaboration.
b. If you want to do "pair programming" on any assignment, that's
fine.
c. Collaborations must be acknowledged.
* If you work as a pair, state that clearly on your solution.
* I will also appreciate a *short* summary of what each person
did.
d. You can use other materials as well (books, papers, stuff from
the web, etc.), but it must be clearly cited.
d. You can see my collaboration policy from CpSc 418 at:
www.ugrad.cs.ubc.ca/~cs418/plagiarism.html