--  $Id: java_concurrency.ty,v 1.8 99/08/10 14:49:08 hnilsson Exp $
-- /***************************************************************************/
-- /*              Copyright (C) 1997-1999 INRIA Sophia-Antipolis             */
-- /*                    I. Attali, D. Caromel and M. Russo                   */
-- /*                              Projet OASIS                               */
-- /*                     2004, route des Lucioles, BP 93,                    */
-- /*                      F-06902 Sophia Antipolis cedex                     */
-- /*                           (+33) 4 92 38 76 31                           */
-- /*                           All rights reserved                           */
-- /***************************************************************************/
--
-- /***************************************************************************/
-- /* Rules for the multi-threading (how the interleaving between threads     */
-- /* must be done). For the moment, all threads have the same priority so    */
-- /* the scheduler chooses the next thread that will become executing.       */
-- /***************************************************************************/
program java_concurrency is
use java;
use PSP;

import
   inf ( _, _ ) , infeq ( _, _ ) , sup ( _, _ ) ,
   supeq ( _, _ ) from arith;

import
   ENVdeleteAThreadFromStackList ( ObjectId ) ,
   ENVsendCurrentExecutingThread ( Objects, ObjectId ) ,
   ENVsendDeadThread ( Objects, ObjectId ) ,
   ENVsendObjectAndClassVariableLists ( Objects, ClassVariablesL ) ,
   ENVupdateThreadStatusList ( ObjectId, ThreadStatus, ThreadStatus ) ,
   ENVupdateEnvIfNonDormantOrBlockedThreadOnObject (
      ObjectId, Objects, integer ) from java_environment;

import
   evaluateExpression (
      Objects, ClassVariablesL, Env, ObjectId, ObjectId, Identifier |-
       SemExpression -> Objects, ClassVariablesL, Env, SemExpression, Insts, ThreadStatus )
   from java_expr_evaluation;

import
   getObject ( ObjectId |- Objects -> Object ) ,
   isTheObjectLocked ( ObjectId |- Objects -> Bool ) ,
   setNewClosure (
      ObjectId, Clr, ClassVariablesL |- Objects -> Objects ) ,
   setNewThreadStatus (
      ObjectId, ThreadStatus, ClassVariablesL |- Objects -> Objects )
   from java_object_list;

import
   executeANonExpression (
      Objects, ClassVariablesL, ObjectId |- Clr -> Objects, ClassVariablesL, Clr, ThreadStatus )
   from java_stat_execution;

import
   getExecutingThread ( _ ) ,
   setNewExecutingThread ( _ )
   from jfunctions;

import appendtree ( _, _, _ ) , diff ( _, _ ) , not_eq ( _, _ )
   from  prolog() ;

var TVCompExpr: SemExpression;
var TVCompStat: SemStatement;
var TVValue: Val;

   set getTheNewExecutingThread is
   --SC: Gets the new executing thread. 
   --SC: Finds in the object list the next executing thread 
   --SC: (chosen scheduler: takes the next thread after the current executing 
   --SC: one in the list. If no thread is found, takes the first one at the 
   --SC: beginning of the list)
   --
   --JC: Class variables 
   --JC: |- Objects 
   --JC: -> Updated object list, Reference of the new executing thread
   judgement ClassVariablesL |- Objects -> Objects, ObjectId;
   --iJC1: Current executing thread reference, Reference of the 
   --iJC1: last thread that can be executed (this information is 
   --iJC1: useful to know if the search must start at the 
   --iJC1: beginning or after the given thread in the object list)
   --iJC1: |- Objects 
   --iJC1: -> New current executing thread, Updated object list 
   judgement ObjectId, ObjectNumber |- Objects -> ObjectId, Objects;
   --iJC2: Objects 
   --iJC2: |- Remaining objects, Current executing thread reference 
   --iJC2: => New executing thread, Updated object list
   judgement Objects |- Objects, ObjectId => ObjectId, Objects;
   --iJC3: Objects 
   --iJC3: |- Remaining objects 
   --iJC3: -> New executing thread, Updated object list
   judgement Objects |- Objects => ObjectId, Objects;

   GetTheNewExecutingThread_EntryPoint:
      canAThreadBeInTheExecutingStatus(
         |- ObjL1 -> true(), LastThreadNb )  &
      getExecutingThread( OThId1 )  &
      OThId1, LastThreadNb |- ObjL1 -> OThId2, ObjL1_1
      --------------------------------
      ClVarL |- ObjL1 -> ObjL1_1, OThId2  ; 
               do
                  ENVsendObjectAndClassVariableLists( ObjL1_1, ClVarL )
                  &
                  ENVsendCurrentExecutingThread( ObjL1_1, OThId2 )
                  &  setNewExecutingThread( OThId2 );

   LookForTheNextExecutingThread_StartAfterTheCurrentThread:
      inf( NbThr, NbLastThr )  &
      ObjL1 |- ObjL1, objectId(true(), objectNumber NbThr) => OThId, ObjL1_1
      --------------------------------
      objectId(true(), objectNumber NbThr), objectNumber NbLastThr |- ObjL1 -> OThId, ObjL1_1  ; 

   LookForTheNextExecutingThread_StartByTheFirstObject:
      supeq( NbThr, NbLastThr )  &  ObjL1 |- ObjL1 => OThId, ObjL1_1
      --------------------------------
      objectId(true(), objectNumber NbThr), objectNumber NbLastThr |- ObjL1 -> OThId, ObjL1_1  ; 

   SeekTheGivenThreadInTheList:
      ObjL1 |- ObjL2, OThId1 => OThId2, ObjL2_1
      --------------------------------
      ObjL1 |- objects[object(ObjId, Type, AttrL, Lock, WaitSet, Activity).ObjL2], OThId1
                  =>
                  OThId2, objects[object(ObjId, Type, AttrL, Lock, WaitSet, Activity).ObjL2_1]  ; 
               provided diff( OThId1, ObjId );

   HasFoundTheGivenThread:
      ObjL1 |- ObjL2 => OThId2, ObjL2_1
      --------------------------------
      ObjL1 |- objects[object(OThId1, Type, AttrL, Lock, WaitSet, Activity).ObjL2], OThId1
                  =>
                  OThId2, objects[object(OThId1, Type, AttrL, Lock, WaitSet, Activity).ObjL2_1]  ; 

   HasFoundTheNextExecutingThread_Runnable:
      _ |- objects[object(OThId, Type, AttrL, Lock, WaitSet, activity(runnable(), Clr)).ObjL] =>
              OThId, objects[object(OThId, Type, AttrL, Lock, WaitSet, activity(executing(), Clr)).ObjL]  ; 
               do
                  ENVupdateThreadStatusList( OThId, runnable(), executing() );

   HasFoundTheNextExecutingThread_Blocked:
      isTheObjectLocked( ObjId |- ObjL1 -> false() )
      --------------------------------
      ObjL1 |- objects[object(OThId, Type, AttrL, Lock, WaitSet, activity(blocked(ObjId), Clr)).ObjL2] =>
                  OThId, objects[object(OThId, Type, AttrL, Lock, WaitSet, activity(executing(), Clr)).ObjL2]  ; 
               do
                  ENVupdateEnvIfNonDormantOrBlockedThreadOnObject(
                     ObjId, ObjL1, 1 )  &
                  ENVupdateThreadStatusList( OThId, blocked(ObjId), executing() );

   BlockedThread_RecursiveRule:
      isTheObjectLocked( ObjId |- ObjL1 -> true() )
      &  ObjL1 |- ObjL2 => OThId2, ObjL2_1
      --------------------------------
      ObjL1 |- objects[object(OThId1, Type, AttrL, Lock, WaitSet, activity(blocked(ObjId), Clr)).ObjL2] =>
                  OThId2, objects[object(OThId1, Type, AttrL, Lock, WaitSet, activity(blocked(ObjId), Clr)).ObjL2_1]  ; 

   ThreadStatusIncompatibleWithTheExecutingStatus_RecursiveRule:
      ObjL1 |- ObjL2 => OThId2, ObjL2_1
      --------------------------------
      ObjL1 |- objects[object(OThId1, Type, AttrL, Lock, WaitSet, activity(ThStatus, Clr)).ObjL2] =>
                  OThId2, objects[object(OThId1, Type, AttrL, Lock, WaitSet, activity(ThStatus, Clr)).ObjL2_1]  ; 
               provided diff( runnable(), ThStatus )  &  not_eq( blocked(_), ThStatus );

   SimpleObject_RecursiveRule:
      ObjL1 |- ObjL2 => OThId, ObjL2_1
      --------------------------------
      ObjL1 |- objects[object(ObjId, Type, AttrL, Lock, WaitSet, empty()).ObjL2] =>
                  OThId, objects[object(ObjId, Type, AttrL, Lock, WaitSet, empty()).ObjL2_1]  ; 
   end getTheNewExecutingThread; 

   set executeThread is
   --SC: Begins the execution of the closure of the current executing thread.
   --
   --JC: Objects, Class varibles, Current executing thread reference 
   --JC: -> Updated object list, Updated class variable list
   judgement (Objects, ClassVariablesL, ObjectId -> Objects, ClassVariablesL);

   GetThread_ExecuteOneStepOfTheClosure:
      getObject(
         OThId |- ObjL1 -> object(OThId, _, _, _, _, activity(_, Closure)) )  &
      executeClosure(
         ObjL1, ClVarL1, OThId |- Closure -> ObjL1_1, ClVarL1_1, _ )
      --------------------------------
      (ObjL1, ClVarL1, OThId -> ObjL1_1, ClVarL1_1)  ; 
               provided
                  ENVdeleteAThreadFromStackList( OThId );
   end executeThread; 

   set executeClosure is
   --SC: First step evaluation for the first instruction of the given closure 
   --SC: (that belongs to the current executing thread). If there is no more 
   --SC: instruction in the given closure, the thread becomes dead.
   --
   --JC: Objects, Class variables, Current executing thread reference 
   --JC: |- Closure of the current executing thread
   --JC: -> Updated object list, Updated class variable list, 
   --JC: New status for the current executing thread
   judgement
      Objects, ClassVariablesL, ObjectId |- Clr -> Objects, ClassVariablesL, ThreadStatus;

   NoMoreInstruction_DeadThread:
      --RC: No more instruction for the current executing thread, so it becomes
      --RC: dead.
      setNewThreadStatus(
         OThId, dead(), ClVarL |- ObjL1 -> ObjL1_1 )  &
      setNewClosure(
         OThId, clr(OThId, Mode, MethName, env(pairs[], locs[]), insts[]), ClVarL |-
          ObjL1_1 -> ObjL1_2 )
      --------------------------------
      ObjL1, ClVarL, OThId |-
       clr(OThId, Mode, MethName, env(_, _), insts[]) -> ObjL1_2, ClVarL, dead()  ; 
               do
                  ENVsendDeadThread( ObjL1_2, OThId )  &
                  ENVdeleteAThreadFromStackList( OThId );

   ExecuteFirstInstructionOfTheClosure:
      executeOneInstruction(
         ObjL1, ClVarL1, OThId |- Clr1 -> ObjL1_1, ClVarL1_1, Clr1_1, ThStatus )
      &
      setNewClosure(
         OThId, Clr1_1, ClVarL1_1 |- ObjL1_1 -> ObjL1_2 )  &
      setNewThreadStatus(
         OThId, ThStatus, ClVarL1_1 |- ObjL1_2 -> ObjL1_3 )
      --------------------------------
      ObjL1, ClVarL1, OThId |- Clr1 -> ObjL1_3, ClVarL1_1, ThStatus  ; 
   end executeClosure; 

   set executeOneInstruction is
   --SC: First step evaluation for the first instruction of the given closure 
   --SC: (that belongs to the current executing thread).
   --
   --JC: Objects, Class variables, Current executing thread reference
   --JC: |- Closure of the current executing thread 
   --JC: -> Updated object list, Updated class variable list, 
   --JC: Updated closure, New status for the current executing thread
   judgement
      Objects, ClassVariablesL, ObjectId |- Clr -> Objects, ClassVariablesL, Clr, ThreadStatus;

   EvaluateExpression_DiscardValue:
      --RC: Note: Exceptions are NOT values in this context ...
      ObjL, ClVarL, OThId |-
       clr(ObjId, Mode, MethName, Env, insts[TVValue.InstL]) ->
          ObjL, ClVarL, clr(ObjId, Mode, MethName, Env, InstL), runnable()  ; 
               provided not_eq( TVValue, except(_, _, _) );

   EvaluateExpression_NotYetAValue:
      evaluateExpression(
         ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
          TVCompExpr -> ObjL1_1, ClVarL1_1, Env1_1, CompExpr_1, InstL2, ThStatus )  &
      appendtree( InstL2, insts[CompExpr_1.InstL1], InstL3 )
      --------------------------------
      ObjL1, ClVarL1, OThId |-
       clr(ObjId, Mode, MethName, Env1, insts[TVCompExpr.InstL1]) ->
          ObjL1_1, ClVarL1_1, clr(ObjId, Mode, MethName, Env1_1, InstL3), ThStatus  ; 

   ExecuteANonExpression:
      executeANonExpression(
         ObjL1, ClVarL1, OThId |-
          clr(ObjId, Mode, MethName, Env, insts[TVCompStat.InstL]) -> ObjL1_1, ClVarL1_1, Clr, ThStatus )
      --------------------------------
      ObjL1, ClVarL1, OThId |-
       clr(ObjId, Mode, MethName, Env, insts[TVCompStat.InstL]) -> ObjL1_1, ClVarL1_1, Clr, ThStatus  ; 
   end executeOneInstruction; 

   set canAThreadBeInTheExecutingStatus is
   --SC: Determines if at least one thread of the object list can become
   --SC: executing (a thread can only become executing when it is runnable
   --SC: or blocked on an unlocked object). Gets also the number of the lattest
   --SC: Thread in the list that can become executing.
   --
   --JC: |- Objects
   --JC: -> True/False, Number of the lattest Thread in the list that can 
   --JC: become executing 
   judgement |- Objects -> Bool, ObjectNumber;
   --iJC: Whole object list, True if a previous thread that become executing/
   --iJC: False, Identifier of this previous thread
   --iJC: |- Objects to analyse
   --iJC: -> True/False
   judgement
      Objects, Bool, ObjectNumber |- Objects -> Bool, ObjectNumber;

   EntryPoint_StartsAnalysis:
      ObjL, false(), objectNumber 0 |- ObjL -> TF, LastThread
      --------------------------------
      |- ObjL -> TF, LastThread  ; 

   NoMoreObjectInTheList:
      _, TF, LastThreadNb |- objects[] -> TF, LastThreadNb  ; 

   SimpleObject_CanNotBecomeExecuting:
      ObjL1, TF1, LastThreadNb1 |- ObjL2 -> TF2, LastThreadNb2
      --------------------------------
      ObjL1, TF1, LastThreadNb1 |-
       objects[object(objectId(false(), _), _, _, _, _, _).ObjL2] -> TF2, LastThreadNb2  ; 

   ThreadBlockedOnALockedObject_CanNotBecomeExecuting:
      isTheObjectLocked( ObjId |- ObjL1 -> true() )
      &  ObjL1, TF1, LastThreadNb1 |- ObjL2 -> TF2, LastThreadNb2
      --------------------------------
      ObjL1, TF1, LastThreadNb1 |-
       objects[object(_, _, _, _, _, activity(blocked(ObjId), _)).ObjL2] -> TF2, LastThreadNb2  ; 

   ThreadNotBlockedOrRunnable_CanNotBecomeExecuting:
      --RC: A thread can only become executing when it is runnable
      --RC: or blocked on an unlocked object.
      ObjL1, TF1, LastThread1 |- ObjL2 -> TF2, LastThread2
      --------------------------------
      ObjL1, TF1, LastThread1 |-
       objects[object(_, _, _, _, _, activity(ThStatus, _)).ObjL2] -> TF2, LastThread2  ; 
               provided diff( ThStatus, runnable() )  &  not_eq( ThStatus, blocked(_) );

   RunnableThread_CanBecomeExecuting:
      ObjL1, true(), OIdNb |- ObjL2 -> true(), LastThread
      --------------------------------
      ObjL1, _, _ |-
       objects[object(objectId(true(), OIdNb), _, _, _, _, activity(runnable(), _)).ObjL2] -> true(), LastThread  ; 

   ThreadBlockedOnANonLockedObject_CanBecomeExecuting:
      isTheObjectLocked( ObjId |- ObjL -> false() )
      &  ObjL1, true(), OIdNb |- ObjL2 -> true(), LastThread
      --------------------------------
      ObjL1, _, _ |-
       objects[object(objectId(true(), OIdNb), _, _, _, _, activity(blocked(ObjId), _)).ObjL2] -> true(), LastThread  ; 
   end canAThreadBeInTheExecutingStatus; 
end java_concurrency