Transcript Applying Formal Methods to Systems

Workshop on the Verification Grand
Challenge
Panagiotis (Pete) Manolios
Georgia Institute of Technology
1
Challenge: A Verified Microprocessor
International Technology Roadmap for Semiconductors,
2003 Edition
Verification has become the dominant cost in the design process. On
current projects, verification engineers outnumber designers, with this
ratio reaching two or three to one for the most complex designs.
...
Without major breakthroughs, verification will be a non-scalable,
show-stopping barrier to further progress in the semiconductor
industry.
…
The overall trend from which these breakthroughs will emerge is the
shift from ad hoc verification methods to more formal ones.
2
Processor Verification
∎ Advantage: The specification is known.
It is the most successful abstraction in CS, the ISA.
∎ Successes:
▮ Boolean equivalence checking.
▮ Floating point verification: AMD, Intel & IBM.
∎ Promising: Term-level reasoning, e.g., UCLID (uses
SAT solvers).
∎ Unsolved: Highly automated reasoning of systemlevel properties of bit-level models.
▮ Unified framework for reasoning at various levels of
abstraction, from netlist to correctness of programs on ISA.
3
Refinement-Based Approach
∎ WEB-Refinement: ISA & implementation have the same visible
behaviors modulo stuttering.
▮ General notion of correctness.
▮ Preservation of safety & liveness properties over CTL* \ X.
∎ Exploiting refinement.
▮ Safety component similar to B&D proofs; we show how to
automatically prove safety & liveness (5% increase in running time).
▮ Separation of concerns: Refinement maps impact verification times:
orders of magnitude improvement over flushing.
▮ Exploiting compositional reasoning.
 Fits into design cycle.
 Allows us to verify machine too complex for state-of-the-art tools.
 Counterexample isolation & simplification.
∎ Improvements in verification times depend not only on decision
procedures: methodological concerns are crucial.
4
Tool Support
∎ Combining ACL2 & UCLID.
∎ ACL2 provides:
▮ Efficient executable models (C-like speed).
▮ Definitional principle guarantees consistency.
▮ Publicly available libraries (e.g., bit-level reasoning using
AMD’s floating point libraries)
∎ UCLID provides:
▮ Term-level automation.
▮ Experiments show substantial performance benefits for CLU.
∎ Challenge: End-to-end arguments.
▮
▮
▮
▮
Prove theorems about code running on micro architecture.
Need theorems about MA we can use, eg, liveness.
Proof decomposition: complete instruction sets.
Evaluate abstractions in context of end-to-end arguments.
5
Education
∎ Goal: undergraduates who verify non-trivial systems.
∎ Public relations/ sociological issue:
▮ Tony Hoare: Correctness of computer programs is the
fundamental concern of the theory of programming...
▮ Most of our colleagues don’t believe this.
▮ Any physicist knows about relativity/ quantum mechanics.
▮ How many CS professionals know basic results of logic /
recursive function theory?
▮ Good news: possible to motivate & train US undergrads.
∎ Mechanical verification for the masses.
▮
▮
▮
▮
▮
Can’t just proselytize; we have to show how it’s done.
Mature system that is self-teaching & gives constant feedback.
We are exploring how to do this with ACL2.
Developing courses, e.g., processor design & verification.
Libraries allow students to focus on big pictures.
6
Grand Challenge Remarks
∎ Objective metric for success.
▮ Choose well-defined collection of problems & specifications.
 Don’t allow rewriting of code / changing specs.
▮
▮
▮
▮
Beyond current reach of current methods: 10K man-years.
Will require significant advances & integration to succeed.
Remove religion: HOL/ FOL/ Model checking/ Rewriting?
Compare approaches by asking:
What % of the problems did you solve?
∎ Sociological aspects of the challenge problems.
▮ Significance should be self-evident to colleagues/funding
agencies. Killer app?
▮ Verify an e-voting (Web-voting) system; health care?
▮ Verify JVM & libraries, e.g., garbage collector, big ints, ….
▮ Build a verified stack: transistors to high-level language
(includes compiler/ OS/ devices & drivers/ applications).
7