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.
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).


  Parameter TMonitor: Set.

An empty monitor
  Parameter newMonitor: TMonitor.

Return the id of the thread which holds the monitor
Returns the number of times the thread which holds the monitor locked it
  Parameter getMonitorLockCount: TMonitornat.

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

  Lemma MonitorInvariant1: m,
    getMonitorThreadId m = NonegetMonitorLockCount m = 0.
    intros m H.

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

Modifies the holder thread id and the lock counter of the monitor
  Parameter setMonitorState: TMonitoroption TThreadIdnatTMonitor.

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

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

  Inductive MonitorLock: TThreadIdTMonitorTMonitorProp :=
  | 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: TThreadIdTMonitorTMonitorProp :=
  | 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: TObjectTClassName.

Returns the monitor state of the given object
  Parameter getObjectMonitor: TObjectTMonitor.

Modifies the monitor state of the given object
  Parameter setObjectMonitor: TObjectTMonitorTObject.

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: TObjectTShortNameoption TValue.

Modifies a field within an object.
  Parameter setObjectField: TObjectTShortNameTValueTObject.


  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: TArrayTType.

Returns the size of an array.
  Parameter getArraySize: TArrayTArraySize.

Reads an array cell.
  Parameter getArrayCell: TArrayTArrayIndexoption 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: TArrayTArrayIndexTAValueTArray.

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: TArrayTArrayIndexoption 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
  | HV_Object (obj: TObject)
  | HV_Array (arr: TArray).


Type of heaps.
  Parameter THeap: Set.

Empty heap.
  Parameter emptyHeap: THeap.

Returns a heap value stored at the given location.
  Parameter get: THeapTThreadIdTLocTHeapValue.

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: THeapTThreadIdTLocTHeapValueTHeap.

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: THeapTLoc.

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: TTypeTArraySizeTArray.

Reads a static field from the heap.
  Parameter getStaticField: THeapTThreadIdTClassNameTShortNameoption TValue.

Writes a value to a static field in the heap and returns the modified heap.
  Parameter setStaticField: THeapTThreadIdTClassNameTShortNameTValueoption THeap.

Reads the special .class field of a class/type, which holds the location of the relevant Class object.
  Parameter getClassObjectLoc: THeapTClassNameoption TLoc.

  Definition getLocClass (h: THeap) (thid: TThreadId) (loc: TLoc): option TClassName :=
    match get h thid loc with
    | HV_Object objSome (getObjectClass obj)
    | _None

  Definition getReferenceType (h: THeap) (thid: TThreadId) (loc: TLoc): option TReferenceType :=
    match get h thid loc with
    | HV_EmptyNone
    | HV_Object objSome (RTObject (getObjectClass obj))
    | HV_Array arrSome (RTArray (getArrayComponentType arr))

systemException (h1 h2: THeap) (exn_loc: TLoc) (exn_cn: TClassName)
  Parameter systemException: THeapTHeapTLocTClassNameProp.


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.
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.
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
        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.

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.
    unfold getReferenceType in H.
    rewrite Pnull_empty in H.
    discriminate H.
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.
  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.