-- $Id: java_object_api.ty,v 1.8 10/.0/.2 .1:.1:.5 mrusso 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 */
-- /***************************************************************************/
--
-- /***************************************************************************/
-- /* This file contains the API specifications for the class Object */
-- /* as well as functionnalities for the WaitSet data */
-- /***************************************************************************/
program java_object_api is
use java;
use PSP;
import
ENVchangeObjectStatusInStatusList ( ObjectId ) ,
ENVsendObjectList ( Objects )
from java_environment;
import
getObject ( ObjectId |- Objects -> Object ) ,
getObjectLockInformation (
ObjectId |- Objects -> ObjectId, integer ) ,
releaseObjectLock ( ObjectId |- Objects -> Objects ) ,
setNewThreadStatus (
ObjectId, ThreadStatus, ClassVariablesL |- Objects -> Objects ) ,
createExceptionObject (
Objects, ObjectId |- Identifier, ExceptText -> ObjectId, Objects, Insts )
from java_object_list;
import appendtree ( _, _, _ ) , diff ( _, _ ) from prolog() ;
set ObjectAPI is
--SC: Performs all the Object constructors and methods.
--
--SC: Specified constructor and methods:
--SC: Object()
--SC: notify()
--SC: notifyAll()
--SC: wait()
--
--JC: Object list, Class variable list, Current executing thread reference,
--JC: Current object reference
--JC: |- Method or Constructor name, Argument list (maybe an empty list)
--JC: -> modified object list, modified class variable list,
--JC: Continuation instruction list (maybe empty), new current Thread status.
judgement
Objects, ClassVariablesL, Ref, Ref |-
Identifier, java -> Objects, ClassVariablesL, Insts, ThreadStatus;
Object:
ObjL, ClVarL, _, ObjId |-
identifier "Object", vals[]
->
ObjL, ClVarL, insts[clr(ObjId, identifier "none", identifier "Object", env(pairs[], locs[]), insts[])], runnable() ;
Notify:
--RC: Wakes up a single thread that is waiting on this object monitor.
--
--CS: ObjId.notify();
--PC: A check is done to be sure that the given object is locked by the
--PC: current executing thread The oldest dormant thread of the wait set
--PC: is taken, its status becomes blocked on 'ObjId' instead of
--PC: dormant=> waiting for nb locks on 'ObjId'.
getObjectLockInformation( ObjId |- ObjL1 -> OThId, nb )
& diff( nb, 0 ) &
makeBlockedTheOldestDormantThread( ObjId |- ObjL1 -> ObjL1_1 )
--------------------------------
ObjL1, ClVarL, OThId, ObjId |-
identifier "notify", vals[] -> ObjL1_1, ClVarL, insts[], runnable() ;
Notify_Exception:
--RC: An exception is thrown because the current object is not locked by
--RC: the current thread. So the Notify() method cannot be executed.
--
--CS: ObjId1.notify();
getObjectLockInformation( ObjId1 |- ObjL1 -> OThId2, _
) & diff( OThId1, OThId2 ) &
createExceptionObject(
ObjL1, OThId1 |-
identifier "IllegalMonitorStateException", exceptText "Method 'notify' called on a non locked object."
->
_, ObjL1_1, InstL )
--------------------------------
ObjL1, ClVarL, OThId1, ObjId1 |-
identifier "notify", vals[] -> ObjL1_1, ClVarL, InstL, runnable() ;
NotifyAll:
--RC: Wakes up all threads that are waiting on this object monitor.
--
--CS: ObjId.notifyAll();
--PC: checks that the given object is locked by the current executing
--PC: thread 'OThId'. Takes all the threads which are in the wait set of
--PC: the object 'ObjId'. Also makes their status blocked on 'ObjId'
--PC: instead of dormant=> waiting for nb locks on 'ObjId'.
getObjectLockInformation( ObjId |- ObjL1 -> OThId, nb )
& diff( nb, 0 ) &
makeBlockedAllDormantThreads( ObjId |- ObjL1 -> ObjL1_1 )
--------------------------------
ObjL1, ClVarL, OThId, ObjId |-
identifier "notifyAll", vals[] -> ObjL1_1, ClVarL, insts[], runnable() ;
NotifyAll_Exception:
--RC: An exception is thrown because the current object is not locked by
--RC: the current thread.
--
--CS : ObjId1.notifyAll();
getObjectLockInformation( ObjId1 |- ObjL1 -> OThId2, 0
) & diff( OThId1, OThId2 ) &
createExceptionObject(
ObjL1, OThId1 |-
identifier "IllegalMonitorStateException", exceptText "Method 'notifyAll' called on a non locked object."
->
_, ObjL1_1, InstL )
--------------------------------
ObjL1, ClVarL, OThId1, ObjId1 |-
identifier "notifyAll", vals[] -> ObjL1_1, ClVarL, InstL, runnable() ;
Wait:
--RC: Makes the current thread "dormant", adds it to the wait set of the current
--RC: object and releases the locks on the current object. The current thread is
--RC: disabled for thread scheduling until another thread call the notifyAll method
--RC: on the current object (or the notify method).
--
--CS: ObjId.wait();
--PC: Checks that the object 'ObjId' is locked by the current executing
--PC: thread 'OThId' and determines how many times the object is locked
--PC: (nb times).
--PC: Adds the thread identifier 'OThId' to the wait set of the object 'ObjId'.
--PC: Releases the nb locks on the object 'ObjId'.
getObjectLockInformation( ObjId |- ObjL1 -> OThId, nb )
& diff( nb, 0 ) &
addThreadToTheObjectWaitSet(
OThId, ObjId |- ObjL1 -> ObjL1_1 ) &
releaseObjectLock( ObjId |- ObjL1_1 -> ObjL1_2 )
--------------------------------
ObjL1, ClVarL, OThId, ObjId |-
identifier "wait", vals[]
->
ObjL1_2, ClVarL, insts[synchroWaitEndRelock(ObjId, integer nb)], dormant(ObjId, integer nb) ;
do
ENVchangeObjectStatusInStatusList( ObjId );
Wait_Exception:
--RC: An exception is thrown because the current object is not locked by
--RC: the current thread.
--
--CS : ObjId1.wait();
getObjectLockInformation( ObjId1 |- ObjL1 -> _, 0 )
&
createExceptionObject(
ObjL1, OThId1 |-
identifier "IllegalMonitorStateException", exceptText "Method 'wait' called on a non locked object."
->
_, ObjL1_1, InstL )
--------------------------------
ObjL1, ClVarL, OThId1, ObjId1 |-
identifier "wait", vals[] -> ObjL1_1, ClVarL, InstL, runnable() ;
end ObjectAPI;
set makeBlockedTheOldestDormantThread is
--SC: Changes the status of the oldest dormant thread of the wait set of the
--SC: given object into blocked
--
--JC: object reference (for which the wait set needs to be changed)
--JC: |- objects of the program
--JC: -> updated object list
--JC: (i.e. the wait set of the given object has changed)
judgement ObjectId |- Objects -> Objects;
--iJC: objects, object reference, the Wait set
--iJC: |- the new Wait Set (empty at the beginning)
--iJC: => updated object list
judgement Objects, ObjectId, Waits |- Waits => Objects;
GetTheWaitSetOfTheGivenObject:
getObject( ObjId |- ObjL1 -> object(ObjId, _, _, _, WaitSet, _) )
& ObjL1, ObjId, waits[] |- WaitSet => ObjL1_1
--------------------------------
ObjId |- ObjL1 -> ObjL1_1 ;
EmptyWaitSet:
ObjL, _, waits[] |- waits[] => ObjL ;
IsTheOldestDormantThread:
setNewThreadStatus(
OThId, blocked(ObjId), classVariablesL[] |- ObjL1 -> ObjL1_1 ) &
setNewWaitSet( ObjL1_1, WaitL |- ObjId -> ObjL1_2 )
--------------------------------
ObjL1, ObjId, WaitL |- waits[OThId] => ObjL1_2 ;
RecursiveRule_NotTheOldestDormantThreadOfTheWaitSet:
appendtree( WaitL1, waits[OThId], WaitL1_1 ) &
ObjL1, ObjId, WaitL1_1 |- OThIdL => ObjL1_1
--------------------------------
ObjL1, ObjId, WaitL1 |- waits[OThId.OThIdL] => ObjL1_1 ;
end makeBlockedTheOldestDormantThread;
set makeBlockedAllDormantThreads is
--SC: Changes the status of all the "dormant" threads of the wait set of the
--SC: given object into blocked. Updates the status list and the
--SC: interpretation environment.
--
--JC1: Object reference
--JC1: |- objects
--JC1: -> updated object list (i.e. all the objects contained in the wait set
--JC1: of the given object have changed their status into blocked)
judgement ObjectId |- Objects -> Objects;
--JC2: Objects, Object reference
--JC2: |- Wait set of the given object
--JC2: => updated object list
judgement Objects, ObjectId |- Waits => Objects;
GetTheObject:
getObject( ObjId1 |- ObjL1 -> object(ObjId1, _, _, _, WaitSet, _) )
& ObjL1, ObjId1 |- WaitSet => ObjL1_1 &
setNewWaitSet( ObjL1_1, waits[] |- ObjId1 -> ObjL1_2 )
--------------------------------
ObjId1 |- ObjL1 -> ObjL1_2 ;
EmptyWaitSet: ObjL, _ |- waits[] => ObjL ;
RecursiveRule_SetBlockedAsStatusInTheWaitSet:
setNewThreadStatus(
OThId, blocked(ObjId), classVariablesL[] |- ObjL1 -> ObjL1_1 ) &
ObjL1_1, ObjId |- OThIdL => ObjL1_2
--------------------------------
ObjL1, ObjId |- waits[OThId.OThIdL] => ObjL1_2 ;
end makeBlockedAllDormantThreads;
set addThreadToTheObjectWaitSet is
--SC: Adds a new thread in the wait set of an object. Updates the object list
--
--JC: Thread reference that needs to be added in the wait set,
--JC: Reference of the object on which this thread wants to set a lock
--JC: |- objects
--JC: -> Updated object list (i.e the wait set of the given object will
--JC: contain the reference of the given thread)
judgement ObjectId, ObjectId |- Objects -> Objects;
GetObject_AddNewThreadInItsWaitSet:
getObject( ObjId |- ObjL1 -> object(ObjId, _, _, _, WaitSet, _) )
&
setNewWaitSet( ObjL1, waits[OThId.WaitSet] |- ObjId -> ObjL1_1 )
--------------------------------
OThId, ObjId |- ObjL1 -> ObjL1_1 ;
end addThreadToTheObjectWaitSet;
set setNewWaitSet is
--SC: Updates the wait set of the given object
--
--JC: Objects, New wait set
--JC: |- Object reference for which the wait set needs to be changed
--JC: -> Modified object list
judgement Objects, Waits |- ObjectId -> Objects;
--iJC:
judgement Objects, Waits |- ObjectId => Objects;
EntryPoint_SendInfoToEnv:
ObjL1, WaitSet |- ObjId => ObjL1_1
--------------------------------
ObjL1, WaitSet |- ObjId -> ObjL1_1 ;
do ENVsendObjectList( ObjL1_1 );
FindTheObject_ChangeItsWaitSet:
objects[object(ObjId, ClName, AttrL, Lock, _, Act).ObjL], WaitSet |-
ObjId => objects[object(ObjId, ClName, AttrL, Lock, WaitSet, Act).ObjL] ;
LookForTheObject:
ObjL1, WaitSet1 |- ObjId1 => ObjL1_1
--------------------------------
objects[object(ObjId2, ClName, AttrL, Lock, WaitSet2, Act).ObjL1], WaitSet1 |-
ObjId1 => objects[object(ObjId2, ClName, AttrL, Lock, WaitSet2, Act).ObjL1_1] ;
provided diff( ObjId1, ObjId2 );
end setNewWaitSet;
end java_object_api