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!