Content-Type: text/enriched
Text-Width: 70
firebrick
MWB: What is it, and what can be learnt?
Björn Victor, Uppsala
firebrick
MWB: What is it, and what can be learnt?
The Mobility Workbench: first tool for pi-calculus
1993-94: proof-of-concept equivalence checker (open bisimulation),
interactive simulation
grey25 BV, FM
1994-95: efficiency efforts, model checker, sort inference
grey25 BV, MD, LHE
1997-98: more efficient model checker, fusion calculus equivalence
grey25 FB, BV
1999: port to SML/NJ 110 (MWB'98)
Used for research and education at darkgreen> 25 sites
darkgreenOn-the-fly algorithms: generate state space while constructing
bisimulation relation or deriving proof
PRO: negative results even on infinite-state (non finite-control)
darkgreen easy
CON: darkgreeninefficient
firebrick
Efficiency:
Classical handover example (37-page hand proof by Orava & Parrow)
1993: on SS10 ~100MHz? > 230 CPU darkgreenhours (didn't terminate)
1995: on SS10: << 11 minutes, 295 Mb memory
2002: on PIII 1.2GHz: ~45 seconds, darkgreen36 Mb memory
How?
firebrick
Efficiency:
Classical handover example (37-page hand proof by Orava & Parrow)
1993: on SS10 ~100MHz? > 230 CPU darkgreenhours (didn't terminate)
1995: on SS10: << 11 minutes, 295 Mb memory
2002: on PIII 1.2GHz: ~45 seconds, darkgreen36 Mb memory
How?
firebrickEfforts:
* 1993-1995: same basic algorithm
- darkgreenterm representation using De Bruijn indicies for names:
no alpha-conversion, "name shifting" (no sharing)
- darkgreennormalisation of terms (push bindings inwards),
darkgreenrewriting to remove true matches, useless restrictions,
deadlocked agents
- hashing techniques for darkgreenrecording all computed transitions
(also of subterms)
Gives darkblue100x speedup for handover example; costs 90% extra memory
(2002; likely more in earlier versions)
* 1995-2002: same code
- speed: MHz
- space: darkgreenmore efficient data structure implementation
(SML/NJ 0.93 vs. 110)
firebrick
Simple lessons:
* Data representation darkbluevery important
* The first three dimensions are most important
- if you have time, buy space
- when you fit, trade space back for time
- if you're lucky, wait and get space and time for free
* Tool architecture: (standard issues)
- design for extensibility (fusion was simple - for me)
- document for others and yourself
darkgreeneven if you think this is only a prototype
- modularise
firebrickTools in PROFUNDIS
New design needed: a tool set (minimum one from each of WP1 and WP2)
Quotes from TA:
darkgreen the intermediate language will include simple data
structures, and allow to embed pi, spi, join, ambients
properties of systems with incomplete information on the
environment, parts added/removed during execution, mobile systems
in particular examples on security properties
automated: model checking, bisimilarity checking, type inference,
proof techniques based on types
semiautomatic: symbolic execution, coinduction proofs (logic)
Goals (examples):
- new applications, formalisms and properties
- higher efficiency
- usability/"exploitation" by other academics
- darkblue(old applications, formalisms and properties)
Needs (examples):
- darkgreenavailability: all development, prototypes, and documentation
must be readily accessible in source to whole project
(and to the public at some point) - no licensed libraries, please!
- darkgreenarchitecture & modularity: distributed implementation
- more darkgreenprecise specifications than TA
firebrickThoughts? Additions? DISCUSS!