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