Library Sem_Monitor

Semantics of monitor instructions

@author Patryk Czarnik, Jacek Chrząszcz

Require Import Logic.
Require Import Relations.
Require Import List.
Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import Heap.
Require Import ZArith.
Require Import Program.
Require Import RuntimeStructures.
Require Import AllStructures.

Module of this type provides detailed semantics of monitor instructions TMonitorInstr.

Module Type SEM_MONITOR.
  Declare Module M_AllStructures : ALL_STRUCTURES.

  Import M_AllStructures.
  Import M_Program.M_ProgramStructures.M_ValuesAndTypes.
  Import M_Program.M_ProgramStructures.
  Import M_ProgramStructuresFacts.
  Import M_Program.
  Import M_RuntimeStructures.M_Heap.
  Import M_RuntimeStructures.

  Open Local Scope Z_scope.
  Import List.ListNotations.

Detailed semantics of I_Monitor instruction, which corresponds to original monitorenter and monitorexit instructions.

Beside direct use from these JVM instruction, this relation is referred in places where the semantics describes synchronized method invocation and aburpt method completion.

Inductive semMonitor : TMonitorOp → TThreadId → TLoc → THeap → TResultOrException THeap → Prop:=

If the thread is no allowed to lock the monitor (and waits), the relation simply does not hold.

  | SemMonitor_lock: ∀ thid loc h h' obj obj' mon mon',
    loc ≠ null →
    get h thid loc = HV_Object obj →
    mon = getObjectMonitor obj →
    MonitorLock thid mon mon' →
    obj' = setObjectMonitor obj mon' →
    h' = set h thid loc (HV_Object obj') →
    semMonitor Op_Lock thid loc h (Result h')

  | SemMonitor_unlock: ∀ thid loc h h' obj obj' mon mon',
    loc ≠ null →
    get h thid loc = HV_Object obj →
    mon = getObjectMonitor obj →
    getMonitorThreadId mon = Some thid →
    MonitorUnlock thid mon mon' →
    obj' = setObjectMonitor obj mon' →
    h' = set h thid loc (HV_Object obj') →
    semMonitor Op_Unlock thid loc h (Result h')

  | SemMonitor_unlock_badThd: ∀ thid other_thid loc h obj mon,
    get h thid loc = HV_Object obj →
    mon = getObjectMonitor obj →
    getMonitorThreadId mon = Some other_thid →
    other_thid ≠ thid →
    semMonitor Op_Unlock thid loc h (Exception StandardNames.IllegalMonitorStateException)

  | SemMonitor_null: ∀ thid h mon_op,
    semMonitor mon_op thid null h (Exception StandardNames.NullPointerException)
  .
End SEM_MONITOR.