Transcript ESC-l9

CS 294-8
Extended Static
Checking
http://www.cs.berkeley.edu/~yelick/294
CS294, Yelick
ESC, p1
Agenda
• Intro and recap
• Overview of ESC (M3 and Java)
• Comparison and Discussion
CS294, Yelick
ESC, p2
Two Themes in Reliable Software
• Limit scope of errors:
– Prevent buggy/malicious app from doing harm to
others
– Both direct (access to data) and indirect
(hogging resources) are important
– The OS may be viewed a special:
• the “trusted arbiter” of limited resources
• Make the program itself run correctly
– Adhere to some reasonable programming
discipline
– Need to specify the discipline
CS294, Yelick
ESC, p3
Dealing with Buggy Software
• Dynamic approaches
–
–
–
–
Restrict access in HW or OS (kernel)
Software Fault Isolation
Checked exceptions and assertions
Virtual machines (e.g., JVM)
• Static approaches
– Type checking
– Verification
– Restricted languages (avoid bugs)
CS294, Yelick
ESC, p4
Recap of Engler Talk
•
•
•
•
How general was the approach?
How useful was it?
What about soundness/completeness?
How could they find bugs in the Flash
code that a “verification” missed?
• What is the right measure of success
for this kind of work? # bugs in
popular code? Others?
CS294, Yelick
ESC, p5
Useful Classes of Rules
• Never/always do X
• Never/always do X before/after Y
• In situation X, do/don’t perform Y
– Use locks; rollback state if failure
• Plus some “optimization-related”
– Do X rather than Y
– In situation Z, do X rather than Y
• How powerful is the language
– For X, Y, Z expressions
– Never/always/when and before/after control
CS294, Yelick
ESC, p6
Extended Static Checking
• Similar goals to the MC work
– Check certain properties of programs
– Not full verification
• Differences
– Requires specifications rather than state
machine
– Uses a theorem prover engine
– Emphasis: control vs. abstraction
– Languages: C vs. M3&Java
CS294, Yelick
ESC, p7
Edit/Prove/Debug Loop
Annotated
Program
Error
message
Verification Condition
Generator
Theorem Prover
Post Processor
CS294, Yelick
“Sorry, can’t
find any
more errors”
ESC, p8
Default Errors in ESC
• ESC acts like a power lint; it checks:
–
–
–
–
–
–
–
Array bounds errors
Subrange errors
Null derefs
Narrowing type cast error
Missing returns
Exceptions not declared
Divide or mod by zero
CS294, Yelick
ESC, p9
ESC Specification Language
• Programmer can add specifications:
–
–
–
–
Procedures and methods
Abstraction
Concurrency
Invariants: loop, module, assertion
• ESC/Java allows for Java expressions
in writing annotations
CS294, Yelick
ESC, p10
Procedures in ESC
• Procedure and methods:
– Modifies: list of all variable that could
be modified
– Requires (precondition)
– Ensures (postcondition)
CS294, Yelick
ESC, p11
ESC/Java Syntax
• Annotations are Java comments with
“@”, I.e., /*@ … */
• 4 categories of annotations (pragmas)
– Lexical: where comments are allowed
– Statement: where statements are
allowed
– Declaration: where declaration of class
and interface members are allowed
– Modifier: within declarations
CS294, Yelick
ESC, p12
ESC/Java Pragmas
• Requires E; assume E in body of method
and warn if can’t be proven at call sites
• Modifies S; will assume calls only modify
these fields (does not check body)
• Ensures E; assumes true after calls, and
proves for body
• Assume E; assume E is true and ignore
branches where it is false
• Assert E; issue a warning if E cannot be
proved
• Nowarn L; turn off these warnings
CS294, Yelick
ESC, p13
Concurrency in ESC
• ESC provides support for concurrent
programs:
– Accessing protected variables without a lock
– Acquiring locks out of order (for deadlock
avoidance)
• The programmer needs to specify
– which variables are protected and
– what order locks should be acquired
• Specified using general axiom facility
– <* SPEC AXIOM (ALL [v: VBT.T] v < v.parent) *>
– Where “<“ denote lock acquisition order
CS294, Yelick
ESC, p14
Concurrency in ESC
• Note that this may be more restrictive
than necessary, but is reasonable (?)
practice.
– Having a global lock acquisition order
– Protecting a shared variable by a fixed lock
• Example:
INTERFACE Rd;
…
TYPE T <: MUTEX;
<* SPEC GetChar(rd)
MODIFIES state[rd]
REQUIRES valid[rd] AND sup(LL) < rd *>
CS294, Yelick
ESC, p15
Concurrency in ESC and MC
• ESC and MC check properties of
concurrent programs, but does not check
the concurrency directly.
– ESC analyzes locks, MC interrupts
– Neither analyze thread creation (e.g., to see if
there is real concurrency)
• Some of the more interesting properties
(and bugs) come from currency
• Are there other common bugs one should
detect?
CS294, Yelick
ESC, p16
Abstractions in ESC
• ESC takes on global analysis and thus
abstraction as a primary focus.
• Problem: specifications need to
describe variable modifications that
are not in scope
• Solution: Use abstract variables in
the specification. May have axioms
on those variables (as in SPEC)
CS294, Yelick
ESC, p17
Data Abstraction in ESC
• Downward closure
– Modifying an abstract variable implies
license to modify concrete ones
• Lack of soundness
– Need to link modifications of concrete
and abstract variables
• Depends maps
DEPENDS Rd.state[rd: Rd.T] ON
rd.st, rd.lo, rd.cur, rd.hi, rd.buff, rd.buff^
CS294, Yelick
ESC, p18
Comparisons to MC
• Could everything done in MC framework be
done in ESC? Consider X after Y
– Make Y’s spec ensure some property “P”
• E.g., interrupt = off
– Make X’s spec ensure ~P
• E.g., interrupt = on
– Give all other procedures
• Requires: interrupt on
• Ensures: interrupt on
• Last point is key to simplicity: property
enforced globally without adding specs
everywhere
CS294, Yelick
ESC, p19
Comparison: ESC and MC
• Choice of language is critical
– Modula 3 and Java, vs.
–C
• Differences in
– Popularity
– Classes of errors that arise
• C is the easy case
CS294, Yelick
ESC, p20
Comparison: ESC and Java
• Difference in background of work
– ESC comes from basic principles
• Theorem proving, verification
– MC comes from systems programming
• How was Exokernel written? What are good
rules to follow in writing systems?
• Related difference
– Effort on the tool vs. effort on the
examples
CS294, Yelick
ESC, p21
Thoughts for Thursday
• Larus will be talking about an
alternate programming style for
servers
– Events vs. threads
– Related to Telegraph, Ninja, others?
• What programming problems likely to
arise in this style?
• How could checkers help?
CS294, Yelick
ESC, p22
Administrivia
• Jim Larus speaking Thursday
– Draft paper online
• Final projects:
– Send mail to schedule meeting with me
• Next week:
– Tuesday ?
– Thursday: Kar and (the other) Hellerstein-- completely
different approach to system reliability
– Following Tuesday: guest lecture by Aaron Brown on
benchmarks; related to Kar and Hellerstein work.
– Still to come: Gray, Lamport, and Liskov
CS294, Yelick
ESC, p23