Transcript retreat - people.csail.mit.edu

unintentional
naming
daniel jackson & sarfraz
khurshid
lcs retreat ·martha’s vineyard · june 2k
alloy project
hypothesis
·better software?
base on clear & simple concepts
elaborate
model
why models?
·smaller & more flexible than code
·can analyze exhaustively
run
analysis
alloy
·a RISC modelling notation
·for structural properties
·SAT-based analyzer
interpret
results
model & issues
2
architecture
design
problem
result
translate
problem
mapping
translate
solution
boolean
formula
SAT
solver
boolean
solution
3
intentional naming case study
why INS?
·naming vital to infrastructure
·INS more powerful than Jini, COM, etc
·the Kaashoek challenge …
what?
·analyzed lookup operation
·based model on SOSP paper & Java code
·a few weeks in April
·Khurshid did all the work
4
intentional naming
attribute/value pairs
city: cambridge
hierarchical specs
city: cambridge, building: ne43, room: 524
service: camera, resolution: hi
service: printer, postscript: level2
lookup
·database maps spec to set of records
·query is set of specs
·lookup returns records meeting all specs
5
tree representation
database
building
ne43
service
camera
n0
n0
query
printer
n1
building
service
ne43
camera
n0 n0
n1
6
strategy
model database & queries
·characterize by constraints
·generate samples
check properties
·obvious
no record returned when no attributes match
·claims
“wildcards are equivalent to omissions”
·essential
additions to DB don’t reduce query results
discuss and refine …
7
alloy model: state
model INS {
domain {Attribute, Value, Record}
state {
Root : fixed Value!
valQ : Attribute? -> Value?
attQ : Value? -> Attribute
valDB : Attribute? -> Value
attDB : Value? -> Attribute
rec : Value + -> Record
lookup : Value -> Record
}
8
alloy model: constraints
// no cycles in query
inv Q4 {no v | v in v.+nextQ}
// if query and DB share a leaf value, lookup returns its
records
inv Lookup1
{all v | no v.attQ || no v.attDB -> v.lookup = v.rec}
// adding a record doesn’t reduce results
assert LookupOK7
{AddRecord -> Root.lookup in Root.lookup'}
9
checking assertions
select
scope
fix
model
run
check
incr
scope
counter?
Y
N
N
real?
slow?
Y
prop
fails
Y
prop
holds
10
3 attrs,
vals, recs
N
results
12 assertions checked
·when query is subtree, ok
·found known bugs in paper
·found bugs in fixes too
·monotonicity violated
11
counterexample
database
size
query
service
service
printer
printer
type
A4
size
mono
n0
n1
A4
n1
12
type
mono
time & effort
costs
 2 weeks modelling, ~100 lines Alloy
cf. 900 lines testing code
 all bugs found in < 10 secs with scope of 4
2 records, 2 attrs, 3 values usually enough
cf. a year of use
 exhausts scope of 5 in 30 secs max
space of approx 10^20 cases
13
lessons

·quick & easy prototyping
·more effective than testing
·assertions easily invented
·visualization a big help

·model not modular
·algorithm a bit tricky
·can’t express paths
14
related experiences
case studies
·microsoft COM: no encapsulation
·collaborative arrival planner: ghost planes
·PANS phone: light gets stuck
other users
·alloy taught in courses at 5 universities
·case studies at: DERA, AT&T, FS, U.Southampton,
Imperial, Oxford
typical dimensions
·model: 20 – 200 lines
·space: 30 – 300 bits
15
helping oxygen?
·rapid experimentation
·articulating essence
·simplifying design
16
musings
why does Alloy help?
lazy specification
refining design ideas
catching showstopper bugs
modelling on the rise?
·tool as trojan horse (SDL, SPIN, SMV)
·design patterns phenomenon
·shop floor to drafting office, c.1850
17