ReferencesStore TypingsSafetyThe Curry-Howard CorrespondenceCIS 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 c hoose OCaml’s style, which is easier to work with formally.So a variable of type T in most languages (exce pt 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 pointer to a cell holding a value of typeT.r =5If this value is “copied” by ass igning it to another variable, the ce llpointed to is not copied.r =5s =So we c an change r by ass igning to s:(s:=6; !r)Aliasing all around usReference cells are not the only language feature that introducesthe possibility of aliasing.IarraysIcommunication channelsII/O devices (disks, etc.)The difficulties of aliasingThe possibility 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:Code motion out of loops, common subexpression elimination,allocation of variables to registers, and detection ofuninitialized variables all depend upon the compiler knowingwhich objects a load or a store ope ration could reference.High-performance compilers spend significant energy 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.Specifically, 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.Specifically, 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.Specifically, 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.Specifically, 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 me mory).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 me mory).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 me mory).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 me mory).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 locationAsideDoes this mean we are going to allow programmers to writeexplicit locations 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