Library Heap

Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import List.
Require Import ZArith.

Heap and objects

@author Patryk Czarnik, Jacek Chrząszcz Module of this type provides definitions for objects and the heap.

Module Type HEAP.

Included modules

In particular, locations are defined in ValuesAndTypes as TLoc.

  Declare Module M_ProgramStructures : PROGRAM_STRUCTURES.
  Import M_ProgramStructures.M_ValuesAndTypes.
  Import M_ProgramStructures.
  Open Local Scope type_scope.

Basic elements

Thread identifier.

Parameter TThreadId: Set.

Thread identifiers are distinguishable.

Axiom PThreadId_eqDec: eqDecS TThreadId.

Index of array cell.

Definition TArrayIndex := M_Numeric_Int.t.

Size of array.

  Definition TArraySize := M_Numeric_Int.t.

  Definition arraySizeFromNat (size: nat) : TArraySize :=
  M_Numeric_Int.const (Z.of_nat size).

Monitors

Parameter TMonitor: Set.

An empty monitor

Parameter newMonitor: TMonitor.

Return the id of the thread which holds the monitor

Parameter getMonitorThreadId: TMonitor → option TThreadId.

Axiom newMonitorThreadId : getMonitorThreadId newMonitor = None.

Returns the number of times the thread which holds the monitor locked it

  Parameter getMonitorLockCount: TMonitor → nat.

  Axiom MonitorInvariant: ∀ m,
    getMonitorThreadId m = None ↔ getMonitorLockCount m = 0.

  Lemma MonitorInvariant1: ∀ m,
    getMonitorThreadId m = None → getMonitorLockCount m = 0.
  Proof.
    intros m H.
    apply → MonitorInvariant.
    assumption.
  Qed.

  Lemma newMonitorLockCount: getMonitorLockCount newMonitor = 0.
  Proof.
    apply MonitorInvariant1.
    apply newMonitorThreadId.
  Qed.

Modifies the holder thread id and the lock counter of the monitor

  Parameter setMonitorState: TMonitor → option TThreadId → nat → TMonitor.

  Axiom getsetMonitorThreadId: ∀ m thid c,
    getMonitorThreadId (setMonitorState m thid c) = thid.

  Axiom getsetMonitorLockCount: ∀ m thid c,
    getMonitorLockCount (setMonitorState m thid c) = c.

  Inductive MonitorLock: TThreadId → TMonitor → TMonitor → Prop :=
  | MonitorLock_free: ∀ thid m,
    getMonitorThreadId m = None →
    MonitorLock thid m (setMonitorState m (Some thid) 1)
  | MonitorLock_owner: ∀ thid m count,
    getMonitorThreadId m = Some thid →
    getMonitorLockCount m = count →
    MonitorLock thid m (setMonitorState m (Some thid) (S count)).

  Inductive MonitorUnlock: TThreadId → TMonitor → TMonitor → Prop :=
  | MonitorUnlock_zero: ∀ thid m,
    getMonitorThreadId m = Some thid →
    getMonitorLockCount m = 1 →
    MonitorUnlock thid m (setMonitorState m None 0)
  | MonitorUnlock_owner: ∀ thid m count,
    getMonitorThreadId m = Some thid →
    getMonitorLockCount m = (S count ) →
    count > 0 →
    MonitorUnlock thid m (setMonitorState m (Some thid) count).

Objects stored in heap

Ordinary objects

Parameter TObject: Set.

Returns the actual ("dynamic") class of an object. The class does not change during the life of an object.

Parameter getObjectClass: TObject → TClassName.

Returns the monitor state of the given object

Parameter getObjectMonitor: TObject → TMonitor.

Modifies the monitor state of the given object

Parameter setObjectMonitor: TObject → TMonitor → TObject.

Returns the value of an instance field. None is returned if such a field is not present for the given object (which is equivalent to being not declared effectively, as declared fields are always initialised in JVM).

Parameter getObjectField: TObject → TShortName → option TValue.

Modifies a field within an object.

Parameter setObjectField: TObject → TShortName → TValue → TObject.

Arrays

Parameter TArray: Set.

Open Local Scope Z_scope.

Index is valid wrt the given size of array.

  Definition validIndex (size: TArraySize) (idx: TArrayIndex): Prop :=
    M_Numeric_Int.toZ idx ≥ 0 ∧
    M_Numeric_Int.toZ idx < M_Numeric_Int.toZ size.
  Close Scope Z_scope.

  Definition validIndexNat (size: TArraySize) (idx: nat): Prop :=
    idx ≥ 0 ∧
    idx < Z.to_nat (M_Numeric_Int.toZ size).

Returns the type of components of an array.

Parameter getArrayComponentType: TArray → TType.

Returns the size of an array.

Parameter getArraySize: TArray → TArraySize.

Reads an array cell.

Parameter getArrayCell: TArray → TArrayIndex → option TAValue.

Writes a value to an array cell. This function does not perform any additional checks; if they are required, they should be done in relevant semantics modules.

Parameter setArrayCell: TArray → TArrayIndex → TAValue → TArray.

Returns the value stored in the given array under the given index. None is returned if the given index is not present (which is equivalent to being out of array boundaries, as array cells are always initialised in JVM).

Parameter getArrayValue: TArray → TArrayIndex → option TValue.

Heap values

Possible values of heap locations.

Inductive THeapValue: Set :=

No value stored. Location not initialised or cleared (which may happen e.g. if garbage collecting is considered).

| HV_Empty

Object.

| HV_Object (obj: TObject)

Array.

| HV_Array (arr: TArray).

Heap

Type of heaps.

Parameter THeap: Set.

Empty heap.

Parameter emptyHeap: THeap.

Returns a heap value stored at the given location.

Parameter get: THeap → TThreadId → TLoc → THeapValue.

Updates a heap location. This is a simple dictionary operation. No preconditions are checked here. If one wants to check e.g. that object of the same class was stored before set, it should be done manually in relevant semantics modules.

Parameter set: THeap → TThreadId → TLoc → THeapValue → THeap.

Returns a fresh location, not used in the heap. In this solution we do not consider object sizes and restrictions for size of heap.

Parameter freshLocation: THeap → TLoc.

Initialises an object according to the given list of fields.

Parameter initObject: list (TShortName × TValue) → TObject.

Initialises an array setting all cells the default value for their kind. initArray componentType size

Parameter initArray: TType → TArraySize → TArray.

Reads a static field from the heap.

Parameter getStaticField: THeap → TThreadId → TClassName → TShortName → option TValue.

Writes a value to a static field in the heap and returns the modified heap.

Parameter setStaticField: THeap → TThreadId → TClassName → TShortName → TValue → option THeap.

Reads the special .class field of a class/type, which holds the location of the relevant Class object.

  Parameter getClassObjectLoc: THeap → TClassName → option TLoc.

  Definition getLocClass (h: THeap) (thid: TThreadId) (loc: TLoc): option TClassName :=
    match get h thid loc with
    | HV_Object obj ⇒ Some (getObjectClass obj)
    | _ ⇒ None
    end.

  Definition getReferenceType (h: THeap) (thid: TThreadId) (loc: TLoc): option TReferenceType :=
    match get h thid loc with
    | HV_Empty ⇒ None
    | HV_Object obj ⇒ Some (RTObject (getObjectClass obj))
    | HV_Array arr ⇒ Some (RTArray (getArrayComponentType arr))
    end.

systemException (h1 h2: THeap) (exn_loc: TLoc) (exn_cn: TClassName)

Parameter systemException: THeap → THeap → TLoc → TClassName → Prop.

Specification

Basic heap specification.

The idea is to specify set/get operations as usual for dictionaries, but so that a change is visible immediatlely only from the current thread. Whether a change is visible from other threads is left unspecified.

It is expected that additional operations will be added to handle synchronistion betwenn thread views of heap.

Additional axiomatisation may also be added to specify more specific models of heap.

  Section HeapSpec.
    Variable h h1 h2: THeap.
    Variable th th1 th2: TThreadId.
    Variable cn cn1 cn2: TClassName.
    Variable fn fn1 fn2: TShortName.
    Variable loc loc1 loc2: TLoc.
    Variable obj obj1 obj2: TObject.
    Variable arr arr1 arr2: TArray.
    Variable idx idx1 idx2: TArrayIndex.
    Variable v v1 v2: TValue.
    Variable va va1 va2: TAValue.
    Variable hval hval1 hval2: THeapValue.
    Variable init_values: list (TShortName × TValue).

An empty heap contains no objects.

Axiom Pempty_empty: get emptyHeap th loc = HV_Empty.

Effect of set is visible from the thread which has invoked it.

    Axiom Pset_get:
      set h1 th loc hval = h2 →
      get h2 th loc = hval.

set does not change other locations (in any thread).

    Axiom Pset_otherLocation:
      loc1 ≠ loc2 →
      set h1 th loc1 hval = h2 →
      get h2 th2 loc2 = get h1 th2 loc2.

freshLocation returns a fresh location (not used even by other threads in the current state of heap.

    Axiom PfreshLocation_fresh:
      freshLocation h = loc →
      get h th loc = HV_Empty.

The null reference is always empty.

Axiom Pnull_empty: get h th null = HV_Empty.

The object returned by initObject is initialised according to fields enumerated in init_values.

    Axiom PinitObject_initialised:
      In (fn , v ) init_values →
      initObject init_values = obj →
      getObjectField obj fn = Some v.

Initialisation does not regard fields not present in init_values. ToThink: Do I really want to guarantee this behaviour? Answer: the right solution is to throw exception on every wrong access.

    Axiom PinitObject_otherFields:
      ¬ In (fn , v ) init_values →
      initObject init_values = obj →
      getObjectField obj fn = None.

    Axiom PsetObjectField_sameField:
      setObjectField obj1 fn v = obj2 →
      getObjectField obj2 fn = Some v.

    Axiom PsetObjectField_otherField:
      fn1 ≠ fn2 →
      setObjectField obj1 fn1 v = obj2 →
      getObjectField obj2 fn2 = getObjectField obj1 fn2.

    Axiom PsetObjectField_Class:
      setObjectField obj1 fn v = obj2 →
      getObjectClass obj2 = getObjectClass obj1.

The array is initialised with values default for given array kind.

    Axiom PinitArray_initialised: ∀ t size idx arr,
      validIndex size idx →
      initArray t size = arr →
      getArrayCell arr idx = Some (defaultArrayValueForType t).

Initialisation does not regard indices outside array boundaries. ToThink: Do I really want to guarantee this behaviour?

    Axiom PinitArray_otherCells: ∀ t size idx arr,
      ¬ validIndex size idx →
      initArray t size = arr →
      getArrayCell arr idx = None.

    Axiom PsetArrayCell_same:
      setArrayCell arr1 idx va = arr2 →
      getArrayCell arr2 idx = Some va.

    Axiom PsetArrayCell_other:
      idx1 ≠ idx2 →
      setArrayCell arr1 idx1 va = arr2 →
      getArrayCell arr2 idx2 = getArrayCell arr1 idx2.

    Axiom PsetArrayCell_size:
      setArrayCell arr1 idx1 va = arr2 →
      getArraySize arr2 = getArraySize arr1.

An empty heap contains no static fields.

Axiom Pempty_empty_static: getStaticField emptyHeap th cn fn = None.

setObjectField does not change other fields (in any thread). Effect of setStaticField is visible from the thread which has invoked it.

    Axiom PsetStaticField_change:
      setStaticField h1 th cn fn v = Some h2 →
      getStaticField h2 th cn fn = Some v.

setStaticField does not change other fields (in any thread).

    Axiom PsetStaticField_otherField:
      fn1 ≠ fn2 →
      setStaticField h1 th cn fn1 v = Some h2 →
      getStaticField h2 th2 cn fn2 = getStaticField h1 th2 cn fn2.

setStaticField does not change fields of other classes (any fields, in any thread).

    Axiom PsetStaticField_otherClass:
      cn1 ≠ cn2 →
      setStaticField h1 th cn1 fn v = Some h2 →
      getStaticField h2 th2 cn2 fn2 = getStaticField h1 th2 cn2 fn2.

    Axiom PsystemException_locationAfter: ∀ h1 h2 exn_loc exn_cn,
      systemException h1 h2 exn_loc exn_cn →
      ∀ thid,
        getReferenceType h2 thid exn_loc = Some (RTObject exn_cn).

    Axiom PsystemException_otherLocations: ∀ h1 h2 exn_loc exn_cn,
      systemException h1 h2 exn_loc exn_cn →
      ∀ loc thid,
        get h1 thid loc ≠ HV_Empty →
        get h2 thid loc = get h1 thid loc.
  End HeapSpec.
End HEAP.

Module HeapFacts (_Heap: HEAP).
  Import _Heap.
  Import M_ProgramStructures.M_ValuesAndTypes.

  Lemma PRefType_NotNull: ∀ h thid loc rt,
    getReferenceType h thid loc = Some rt →
    loc ≠ null.
  Proof.
    intros.
    intro.
    subst.
    unfold getReferenceType in H.
    rewrite Pnull_empty in H.
    discriminate H.
  Qed.
End HeapFacts.

Specification of monolitic heap

This module extends HEAP with additional axiomatisation making the heap fully synchronised -- all threads have the same view of the heap.

Module Type MONOLITIC_HEAP.
  Include HEAP.
  Import M_ProgramStructures.M_ValuesAndTypes.
  Import M_ProgramStructures.

  Section MonoHeapSpec.
    Variable h: THeap.
    Variable loc: TLoc.
    Variable th1 th2: TThreadId.
    Variable cn: TClassName.
    Variable fn: TShortName.
    Variable hv: THeapValue.
    Variable v: TValue.
    Variable init_values: list (TShortName × TValue).

    Axiom Pget_mono:
      get h th1 loc = get h th2 loc.

    Axiom PgetStaticField_mono:
      getStaticField h th1 cn fn = getStaticField h th2 cn fn.

    Axiom Pset_mono:
      set h th1 loc hv = set h th2 loc hv.

    Axiom PsetStaticField_mono:
      setStaticField h th1 cn fn v = setStaticField h th2 cn fn v.
  End MonoHeapSpec.
End MONOLITIC_HEAP.