daniel jackson & sarfraz khurshidlcs retreat ·martha’s vineyard · june 2k

unintentionalnaming

alloy project

hypothesis
• better software?
  base on clear & simple concepts
  

why models?
• smaller & more flexible than code
• can analyze exhaustively

alloy
• a RISC modelling notation
• for structural properties
• SAT-based analyzer

architecture

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

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

tree representation

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 …

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 }

alloy model: constraints

// no cycles in queryinv Q4 {no v | v in v.+nextQ}

// if query and DB share a leaf value, lookup returns its recordsinv Lookup1 {all v | no v.attQ || no v.attDB -> v.lookup = v.rec}

// adding a record doesn’t reduce resultsassert LookupOK7 {AddRecord -> Root.lookup in Root.lookup'}

checking assertions

selectscope

runcheck

counter?

fixmodel

slow?

real?

incrscope

propfails

propholds

Y

Y

N

N

Y

N

3 attrs,vals, recs

results

12 assertions checked
• when query is subtree, ok
• found known bugs in paper
• found bugs in fixes too
• monotonicity violated

counterexample

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

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

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

helping oxygen?

• rapid experimentation
• articulating essence
• simplifying design

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