CIS 500Software FoundationsFall 2006October 18ReferencesMutabilityIIn most programming languages, variables are mutable — i.e.,a variable provides bothIa name that refers to a previously calculated value, andIthe possibility of overwriting this value with another (whichwill be referred to by the same name)IIn some languages (e.g., OCaml), these features are separate:Ivariables are only for naming — the binding between a variableand its value is immutableIintroduce a new class of mutable values (called reference cellsor references)Iat any given moment, a reference holds a value (and can bedereferenced to obtain this value)Ia new value may be assigned to a referenceWe choose OCaml’s style, which is easier to work with formally.So a variable of type T in most languages (except OCaml) willcorrespond to a Ref T (actually, a Ref(Option T)) here.Basic Examplesr = ref 5!rr := 7(r:=succ(!r); !r)(r:=succ(!r); r:=succ(!r); r:=succ(!r);r:=succ(!r); !r)i.e.,((((r:=succ(!r); r:=succ(!r)); r:=succ(!r));r:=succ(!r)); !r)Basic Examplesr = ref 5!rr := 7(r:=succ(!r); !r)(r:=succ(!r); r:=succ(!r); r:=succ(!r);r:=succ(!r); !r)i.e.,((((r:=succ(!r); r:=succ(!r)); r:=succ(!r));r:=succ(!r)); !r)AliasingA value of type Ref T is a p ointe r to a c ell holding a value of typeT.r =5If this value is “copied” by assigning it to another variable, the cellpointe d to is not copied.r =5s =So we can change r by assigning to s:(s:=6; !r)Aliasing all around usReference cells are not the only language feature that introducesthe p oss ibility of aliasing.IarraysIcommunication channelsII/O devices (disks, etc.)The difficulties of aliasingThe pos sibility of aliasing invalidates all sorts of useful forms ofreasoning about programs, both by programmers...The functionλr:Ref Nat. λs:Ref Nat. (r:=2; s:=3; !r)always returns 2 unless r and s are aliases....and by compilers:Co de m otion out of loops, common subexpression elimination,alloc ation of variables to regist ers, and detect ion ofuninitialized variables all depend upon the compiler knowingwhich objects a load or a store operation could reference.High-p erformance compilers sp end significant e nergy on aliasanalysis to try to establish when different variables cannot possiblyrefer to the same storage.The benefits of aliasingThe problems of aliasing have led some language designers simplyto disallow it (e.g., Haskell).But there are good reasons why most languages do provideconstructs involving aliasing:Iefficiency (e.g., arrays)I“action at a distance” (e.g., symbol tables)Ishared resources (e.g., locks) in concurrent systemsIetc.Examplec = ref 0incc = λx:Unit. (c := succ (!c); !c)decc = λx:Unit. (c := pred (!c); !c)incc unitdecc unito = {i = incc, d = decc}let newcounter =λ_:Unit.let c = ref 0 inlet incc = λx:Unit. (c := succ (!c); !c) inlet decc = λx:Unit. (c := pred (!c); !c) inlet o = {i = incc, d = decc} inoSyntaxt ::= termsunit unit constantx variableλx:T.t abstractiont t applicationref t reference creation!t dereferencet:=t assignment... plus other familiar types, in examples.Typing RulesΓ ` t1: T1Γ ` ref t1: Ref T1(T-Ref)Γ ` t1: Ref T1Γ ` !t1: T1(T-Deref)Γ ` t1: Ref T1Γ ` t2: T1Γ ` t1:=t2: Unit(T-Assign)Final exampleNatArray = Ref (Nat→Nat);newarray = λ_:Unit. ref (λn:Nat.0);: Unit → NatArraylookup = λa:NatArray. λn:Nat. (!a) n;: NatArray → Nat → Natupdate = λa:NatArray. λm:Nat. λv:Nat.let oldf = !a ina := (λn:Nat. if equal m n then v else oldf n);: NatArray → Nat → Nat → UnitEvaluationWhat is the value of the expression ref 0?Crucial observation: evaluating ref 0 must do something.Otherwise,r = ref 0s = ref 0andr = ref 0s = rwould behave the same.Spec ifically, evaluating ref 0 should allocate some storage andyield a reference (or pointer) to that storage.So what is a reference?EvaluationWhat is the value of the expression ref 0?Crucial observation: evaluating ref 0 must do something.Otherwise,r = ref 0s = ref 0andr = ref 0s = rwould behave the same.Spec ifically, evaluating ref 0 should allocate some storage andyield a reference (or pointer) to that storage.So what is a reference?EvaluationWhat is the value of the expression ref 0?Crucial observation: evaluating ref 0 must do something.Otherwise,r = ref 0s = ref 0andr = ref 0s = rwould behave the same.Spec ifically, evaluating ref 0 should allocate some storage andyield a reference (or pointer) to that storage.So what is a reference?EvaluationWhat is the value of the expression ref 0?Crucial observation: evaluating ref 0 must do something.Otherwise,r = ref 0s = ref 0andr = ref 0s = rwould behave the same.Spec ifically, evaluating ref 0 should allocate some storage andyield a reference (or pointer) to that storage.So what is a reference?The StoreA reference names a location in the store (also known as the heapor just the memory).What is the store?IConcretely: An array of 8-bit bytes, indexed by 32-bitintegers.IMore abstractly: an array of valuesIEven more abstractly: a partial function from locations tovalues.The StoreA reference names a location in the store (also known as the heapor just the memory).What is the store?IConcretely: An array of 8-bit bytes, indexed by 32-bitintegers.IMore abstractly: an array of valuesIEven more abstractly: a partial function from locations tovalues.The StoreA reference names a location in the store (also known as the heapor just the memory).What is the store?IConcretely: An array of 8-bit bytes, indexed by 32-bitintegers.IMore abstractly: an array of valuesIEven more abstractly: a partial function from locations tovalues.The StoreA reference names a location in the store (also known as the heapor just the memory).What is the store?IConcretely: An array of 8-bit bytes, indexed by 32-bitintegers.IMore abstractly: an array of valuesIEven more abstractly: a partial function from locations tovalues.LocationsSyntax of values:v ::= valuesunit unit constantλx:T.t abstraction valuel store location... and since all values are terms...Syntax of Termst ::= termsunit unit constantx variableλx:T.t abstractiont t applicationref t reference creation!t dereferencet:=t assignmentl store locationAsideDo es this mean we are going to allow programmers to writeexplicit lo c ations in their programs??No: This is just a modeling trick. We are enriching the “sourcelanguage” to include some run-time structures, so that we cancontinue to formalize evaluation as a relation between sourceterms.Aside: If we formalize evaluation in the big-step