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