Weak updates and separation logicGang Tan1, Zhong Shao2, Xinyu Feng3, and Hongxu Cai41Lehigh University,2Yale University3Toyota Technological Institute at Chicago,4Google Inc.Abstract. Separation Logic (SL) provides a simple but powerful technique forreasoning about imperative programs that use shared data structures. Unfortu-nately, SL supports only “strong updates”, in which mutation to a heap locationis safe only if a unique reference is owned. This limits the applicability of SLwhen reasoning about the interaction between many high-level languages (e.g.,ML, Java, C#) and low-level ones since these high-level languages do not supportstrong updates. Instead, they adopt the discipline of “weak updates”, in whichthere is a global “heap type” to enforce the invariant of type-preserving heap up-dates. We present SLw, a logic that extends SL with reference types and elegantlyreasons about the interaction between strong and weak updates. We also describea semantic framework for reference types; this framework is used to prove thesoundness of SLw.1 IntroductionReasoning about mutable, aliased heap data structures is essential for proving propertiesor checking safety of imperative programs. Two distinct approaches perform such kindof reasoning: Separation Logic, and a type-based approach employed by many high-level programming languages.Extending Hoare Logic, the seminal work of Separation Logic (SL [10, 13]) is apowerful framework for proving properties of low-level imperative programs. Throughits separating conjunction operator and frame rule, SL supports local reasoning aboutheap updates, storage allocation, and explicit storage deallocation.SL supports “strong updates”: as long as a unique reference to a heap cell is owned,the heap-update rule of SL allows the cell to be updated with any value:{(e 7→ −) ∗ p}[e] := e′{(e 7→ e′) ∗ p} (1)In the above heap-update rule, there is no restriction on the new value e′. Hereafter, werefer to heaps with strong updates as strong heaps. Heap cells in strong heaps can holdvalues of different types at different times of program execution.Most high-levelprogramming languages (e.g., Java, C#, and ML), however, supportonly “weak updates”. In this paradigm, programs can perform only type-preservingheap updates. There is a global “heap type” that tells the type of every allocated heaplocation. The contents at a location have to obey the prescribed type of the location inthe heap type, at any time. Managing heaps with weak updates is a simple and type-safe mechanism for programmers to access memory. As an example, suppose an MLvariable has type “τ ref” (i.e., it is a reference to a value of type τ). Then any updatethrough this reference with a new value of type τ is type safe and does not affect othertypes, even in the presence of aliases and complicated points-to relations. Hereafter, werefer to heaps with weak updates as weak heaps.This paper is concerned with the interaction between strong and weak updates.Strong-update techniques are more precise and powerful, allowing destructive mem-ory updates and explicit deallocation. But aliases and uniqueness have to be explic-itly tracked. Weak-update techniques allow type-safe management of memory withouttracking aliases, but types of memory cells can never change. A framework that mixesstrong and weak updates enables a trade-off between precision and scalability.Such a framework is also useful for reasoning about multilingual programs. Mostreal-world programs are developed in multiple programming languages. Almost allhigh-level languages provide foreign function interfaces for interfacing with low-levelC code (for example, the OCaml/C FFI, and the Java Native Interface). Real-worldprograms consist of a mixture of code in both high-level and low-level languages. Aruntime state for such a program conceptually contains a union of a weak heap and astrong heap. The weak heap is managed by a high-level language (e.g., Java), acceptstype-preserving heap updates, and is garbage-collected. The strong heap is managedby a low-level language, accepts strong updates, and its heap cells are manually recol-lected. To check the safety and correctness of multilingual programs, it is of practicalvalue to have one framework that accommodates both strong and weak updates.Since Separation Logic (SL) supports strong heaps, one natural thought to mixstrong and weak updates is to extend SL with types so that assertions can also de-scribe weak heaps. That is, in addition to regular SL assertions, we add {e 7→ τ}, whichspecifies a heap with a single cell and the cell holds a value of type τ. This scheme,however, would encounter two challenges.First, allowing general reference types in {e 7→ τ} would make SL unsound. Anexample demonstrating this point is as follows:{{x 7→ 4} ∗ {y 7→ even ref}} [x] := 3 {{x 7→ 3} ∗ {y 7→ even ref}} (2)The example is an instantiation of the heap-update rule in (1) and uses the additionalassertion {e 7→ τ}. The precondition states that y points to a heap cell whose contentsare of type “even ref” (i.e., a reference to an even integer). Therefore, the preconditionis met on a heap where y points to x. However, the postcondition will not hold on thenew heap after the update because x will point to an odd number. Therefore, the aboverule is sound only if y does not point to x.The second challenge of adding types to SL is how to prove its soundness withmixed SL assertions and types. Type systems are usually proved sound following asyntactic approach [19], where types are treated as syntax. Following the tradition ofHoare Logic, SL’s soundness is proved through a denotational model, and SL assertionsare interpreted semantically. There is a need to resolve the conflict between syntacticand semantic soundness proofs.In this paper, we propose a hybrid logic, SLw, which mixes SL and a type system.Although the logic is described in a minimal language and type system, it makes a solidstep toward a framework that reasons about the interaction between high-level and low-level languages. The most significant technical aspects of the logic are as follows:2(Command) c ::= ··· | x := [e] | [x] := e | x := alloc(e) | free(e)(Expression) e ::= x | v | op(e1,...,en)(Value) v ::= n | ℓFig.1. Language syntax– SLwextends SL with a simple type system. It employs SL for reasoning aboutstrong updates, and employs the type system for weak updates.