March 13, 2006 http://csg.csail.mit.edu/6.375/ L13-1Bluespec-7: Semantics of BluespecArvind Computer Science & Artificial Intelligence LabMassachusetts Institute of TechnologyMarch 13, 2006 L13-2http://csg.csail.mit.edu/6.375/TopicsGuarded actions versus Conditional actionsNaming expressions: the “let” statementModules and methods with implicit conditionsRule compositionMarch 13, 2006 L13-3http://csg.csail.mit.edu/6.375/BS0: A simple language of Guarded Atomic Actionsa is an Action; e is an Expression; r is a register (state variable)a ::= r := e | a when e | if e then a | a ; ae ::= r | c | Op(e , e ) | e ? e : e | e when e | ...“;” is commutative and associative, i.e.a1;a2 = a2;a1a1;(a2;a3) = (a1;a2);a3action a is guarded by predicate ecompound atomic actionconditional actionconditional expressionguarded expressionMarch 13, 2006 L13-4http://csg.csail.mit.edu/6.375/BS0ProgramA program is a collection of registers and rules: R, R1, R2, ... are names for rules;r, r1, r2, ... are register namesProgram ::= Registers r1, ..., ;Rule R1a1; ... ; Rule Rmam;a ::= r := e | a when e | if e then a | a ; a e ::= r | c | Op(ra, rb) | e ? e : e | e when e | ...March 13, 2006 L13-5http://csg.csail.mit.edu/6.375/Guards vs If’sA guard on one action of a group of actions affects every action within the group(a1 when p1); (a2 when p2) ==> (a1; a2) when p1 & p2A condition of a Conditional action only affects the actions within the scope of the conditional action(if p1 then a1); (if p2 then a2)p1 has no effect on a2 ... March 13, 2006 L13-6http://csg.csail.mit.edu/6.375/Canonicalizing BS0ignoring guards on expressionsRules for canonicalization:1. (a1 when p); a2 ==> (a1; a2) when p2. (a when p1) when p2 ==> a when (p1 & p2)3. if p then (a when q) ==> (if p then a) when (p&q | !p)March 13, 2006 L13-7http://csg.csail.mit.edu/6.375/Conditionals & Casesif p then a1 else a2= if p then a1; if !p then a2Similarly for casesMarch 13, 2006 L13-8http://csg.csail.mit.edu/6.375/BS0: Canonical formIn the canonical form, expressions have no guards and an (or a compound) action has at most one guard and it occurs at the top level;ag is an Action with guarda is an Action without guard; e is an Expression; r is a register (state variable)ag::= a when ea ::= r := e | if e then a | a ; ae ::= r | c | Op(e , e ) | e ? e : e | ...move all the guards to the top levelMarch 13, 2006 L13-9http://csg.csail.mit.edu/6.375/Rules for Canonicalizing BS01. (a1 when p); a2 ==> (a1; a2) when p2.1 (a when p) when q ==> a when (p & q)2.2 (e when p) when q ==> e when (p & q)3.1 if p then (a when q) ==> (if p then a) when (p&q | !p)3.2 p ? (e1 when q) : e2 ==> (p ? e1 : e2) when (p&q | !p)3.3 p ? e1 : (e2 when q) ==> (p ? e1 : e2) when (p | !p&q)4 r := (e when q) ==> (r := e) when q5.1 Op(e1 when q, e2) ==> Op(e1,e2) when q5.2 Op(e1, e2 when q) ==> Op(e1,e2) when q5.3 if (p when q) then a ==> (if p then a) when q5.4 (p when q)? e1 : e2 ==> (p ? e1 : e2) when qTheorem: Canonical form for an action exists and is unique up to the boolean simplification of the guard expression. March 13, 2006 L13-10http://csg.csail.mit.edu/6.375/BS1= BS0+ Let blocks Introducing local namest, t1, t2, ... are identifiers (not registers)Program ::= Registers r1, ..., ;t1= e1; ...; tn= en; Rule R1a1; ... ; Rule Rmam;a ::= r := e | a when e | if e then a | a ; a | (t1= e1; ...; tn= en; in a)e ::= r | c | Op(ra, rb) | e ? e : e | e when e | ... | t | (t1= e1; ...; tn= en; in e)March 13, 2006 L13-11http://csg.csail.mit.edu/6.375/BS1Lifting rulesUnique local names (t1, t2, ...) can be introduced anywhere for sharinge ==> (t = e in t)Lifting rules for actions r:= (t = e in e’) ==> (t = e in r:=e’) a when (t = e in e’) ==> (t = e in (a when e’)) (t = e in (e’ when p)) ==> (t = e in e’) when p if (t=e in p) then e1 ==> (t = e in (if p then e1)) (t = e in a1); a2 ==> (t = e in (a1;a2)) (t1 = e1 in (t2 = e2 in a)) ==> (t1 = e1; t2 = e2 in a)Some renaming of local variables may be requiredSubstitution & when clauses (t=e when p in e’) ==> (t = e; t1 = p in [(t when t1)/t]e’)Lifting rules for expressions are similarMarch 13, 2006 L13-12http://csg.csail.mit.edu/6.375/Lifting lets to the top levelRegisters r1, ..., ;t1= e1; ...; tn= en; Rule R1a1; ... ; Rule Rmam;Rule Ri(ti1= ei1; ...; tin= ein; in ai)==> Registers r1, ..., ;t1= e1 ; ...; tn= en ; ti1= ei1; ...; tin= ein; Rule R1a1; ... ; Rule Rmam;Rule RiaiSome renaming of local variables may be requiredMarch 13, 2006 L13-13http://csg.csail.mit.edu/6.375/BS1: Canonical formProgram ::= Registers r1, ..., ;t1= e1; ...; tn= en; Rule R1ac1; ... ; Rule Rmacm;ac ::= (t1= e1; ...; tn= en; in aw)ac’::= (t1= e1; ...; tn= en; in a)aw ::= a | a when e a ::= r := e | if e then ac’ | a ; a ec ::= (t1= e1; ...; tn= en; in ew)ec’::= (t1= e1; ...; tn= en; in e)ew::= e | e when p e ::= r | c | Op(ra, rb) | e ? ec’ : ec’... | t March 13, 2006 L13-14http://csg.csail.mit.edu/6.375/BS2= BS1+ ModulesA program is a collection of (instantiated) modules m, m1,...;A module is a collection of rules and interface methods f, f1, f2, ... are names for “read methods”g, g1, g2, ... are names for “action methods”a ::= r := e | a when e | if e then a | a ; a | (t = e in a)| m.g(e)e ::= r | c | Op(ra, rb) | e ? e : e | ... | e when e | t | (t = e in e) |m.f(e) March 13, 2006 L13-15http://csg.csail.mit.edu/6.375/BS2ProgramA program is a collection of instantiated modules: Program ::= m1; m2; m2; ...Module ::= Module name[Register r][Rule R a];InterfaceInterface ::= [action method]; [read method]action method ::= method g (x) = aread method ::= method f (x) = eMarch 13, 2006 L13-16http://csg.csail.mit.edu/6.375/Implicit conditionsEvery method has two parts: guard and body. These will be designated by subscripts G and B, respectivelyMaking guards explicit in every method call:m.h(e) ==> (p = m.hGin m.hB(e) when p)March 13, 2006 L13-17http://csg.csail.mit.edu/6.375/BS2: Additional Lifting rulesOnly read methods can be named in a let blockm.f(e) ==> (t=m.f(e) in t)m.g (t = e in e’) ==> (t = e in m.g(e’))m.g (e when p) ==> m.g(e) when p similar rules for read methodsMarch 13, 2006 L13-18http://csg.csail.mit.edu/6.375/Some subtle issuesDoes it matter if we first make the guards explicit and then lift or can we lift at any stage?March 13, 2006 L13-19http://csg.csail.mit.edu/6.375/BS2:
View Full Document
Unlocking...