001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.jvm;
020:
021: import gov.nasa.jpf.JPFException;
022: import gov.nasa.jpf.util.Debug;
023: import gov.nasa.jpf.util.HashData;
024:
025: /**
026: * Represents the monitor associate with classes and objects.
027: */
028: public class Monitor {
029: /**
030: * The identifier of the thread locking an object.
031: */
032: private int lockingThread;
033:
034: /**
035: * The number of nested locks acquired.
036: */
037: private int lockCount;
038:
039: /**
040: * The list of threads waiting to be notified.
041: */
042: private int[] waitingThreads;
043:
044: /**
045: * Creates a new empty monitor.
046: */
047: public Monitor() {
048: lockingThread = -1;
049: lockCount = 0;
050: waitingThreads = new int[0];
051: }
052:
053: /**
054: * Returns the number of nested locks acquired.
055: */
056: public int getLockCount() {
057: return lockCount;
058: }
059:
060: /**
061: * Returns the identifier of the thread holding the lock.
062: */
063: public int getLockingThread() {
064: return lockingThread;
065: }
066:
067: /**
068: * Returns the list of waiting threads.
069: */
070: public int[] getWaitingThreads() {
071: return waitingThreads;
072: }
073:
074: /**
075: * Returns true if it is possible to lock the monitor.
076: */
077: public boolean canLock(ThreadInfo th) {
078: if (lockingThread == -1) {
079: return true;
080: }
081:
082: return (lockingThread == th.index);
083: }
084:
085: /**
086: * Creates a clone of the monitor.
087: */
088: public Object clone() {
089: Monitor m = new Monitor();
090:
091: m.lockingThread = lockingThread;
092: m.lockCount = lockCount;
093: m.waitingThreads = new int[waitingThreads.length];
094: System.arraycopy(waitingThreads, 0, m.waitingThreads, 0,
095: waitingThreads.length);
096:
097: return m;
098: }
099:
100: /**
101: * Compares to another object.
102: */
103: public boolean equals(Object o) {
104: if (o == null) {
105: return false;
106: }
107:
108: if (!(o instanceof Monitor)) {
109: return false;
110: }
111:
112: Monitor m = (Monitor) o;
113:
114: if (lockingThread != m.getLockingThread()) {
115: return false;
116: }
117:
118: if (lockCount != m.getLockCount()) {
119: return false;
120: }
121:
122: int[] w = m.waitingThreads;
123:
124: if (waitingThreads.length != w.length) {
125: return false;
126: }
127:
128: for (int i = 0; i < waitingThreads.length; i++) {
129: if (waitingThreads[i] != w[i]) {
130: return false;
131: }
132: }
133:
134: return true;
135: }
136:
137: public void hash(HashData hd) {
138: hd.add(lockingThread);
139: hd.add(lockCount);
140:
141: for (int i = 0, l = waitingThreads.length; i < l; i++) {
142: hd.add(waitingThreads[i]);
143: }
144: }
145:
146: public int hashCode() {
147: HashData hd = new HashData();
148:
149: hash(hd);
150:
151: return hd.getValue();
152: }
153:
154: /**
155: * Interrupts one of the threads holding the lock.
156: */
157: public void interrupt(ThreadInfo th) {
158: remove(th.index);
159: th.setStatus(ThreadInfo.INTERRUPTED);
160: }
161:
162: /**
163: * Acquires the lock for a given object or class.
164: */
165: public void lock(ThreadInfo th, Ref ref) {
166: // in general, locking is only permitted from the currently running thread
167: // in case the object isn't locked yet.
168:
169: if (lockingThread == -1) {
170: lockingThread = th.index;
171:
172: th.lock(ref);
173: } else if (lockingThread != th.index) {
174: throw new JPFException("lock operation failed");
175: }
176:
177: lockCount++;
178: }
179:
180: /**
181: * Tries to re-aquire the lock after being notified.
182: */
183: public void lockNotified(ThreadInfo th, Ref ref) {
184: if (lockingThread != -1) {
185: throw new JPFException("lock operation failed");
186: }
187:
188: lockingThread = th.index;
189: lockCount = th.getLockCount();
190:
191: //** warning: should have been done when interrupted was set. **//
192: for (int i = 0; i < waitingThreads.length; i++) {
193: if (waitingThreads[i] == th.index) {
194: remove(i);
195:
196: break;
197: }
198: }
199:
200: th.setStatus(ThreadInfo.RUNNING);
201: th.setLockCount(0);
202:
203: th.lock(ref);
204: }
205:
206: public void log() {
207: Debug.println(Debug.MESSAGE, " $lockingThread$: "
208: + lockingThread);
209: Debug.println(Debug.MESSAGE, " $lockCount$: " + lockCount);
210: Debug.print(Debug.MESSAGE, " $waitingThreads$: { ");
211:
212: for (int i = 0, l = waitingThreads.length; i < l; i++) {
213: if (i != 0) {
214: Debug.print(Debug.MESSAGE, ", ");
215: }
216:
217: Debug.print(Debug.MESSAGE, Integer
218: .toString(waitingThreads[i]));
219: }
220:
221: Debug.println(Debug.MESSAGE, " }");
222: }
223:
224: /**
225: * Notifies one of the threads. The thread is chosen non deterministically.
226: */
227: public void notify(SystemState ss) {
228: int length = waitingThreads.length;
229:
230: if (length == 0) {
231: return;
232: }
233:
234: int random = ss.random(length);
235:
236: ss.ks.tl.get(remove(random)).setStatus(ThreadInfo.NOTIFIED);
237: }
238:
239: /**
240: * Notifies all waiting threads.
241: */
242: public void notifyAll(SystemState ss) {
243: for (int i = 0, l = waitingThreads.length; i < l; i++) {
244: ThreadInfo th = ss.ks.tl.get(waitingThreads[i]);
245: th.setStatus(ThreadInfo.NOTIFIED);
246: }
247:
248: waitingThreads = new int[0];
249: }
250:
251: public int objectHashCode() {
252: return super .hashCode();
253: }
254:
255: public String toString() {
256: StringBuffer sb = new StringBuffer();
257:
258: sb.append("Monitor(");
259: sb.append("lockingThread=");
260: sb.append(lockingThread);
261: sb.append(',');
262: sb.append("lockCount=");
263: sb.append(lockCount);
264: sb.append(',');
265: sb.append("waitingThreads=");
266: sb.append('[');
267:
268: for (int i = 0; i < waitingThreads.length; i++) {
269: if (i != 0) {
270: sb.append(',');
271: }
272:
273: sb.append(waitingThreads[i]);
274: }
275:
276: sb.append(']');
277: sb.append(')');
278:
279: return sb.toString();
280: }
281:
282: /**
283: * Releases the lock. The lock can be still held by the thread
284: * if it had been locked more than once.
285: */
286: public void unlock(ThreadInfo th, Ref ref) {
287: // <2do> - might actually be a better way to deal with synced native
288: // methods giving up the lock (join)
289: //if (lockingThread == -1) return;
290:
291: lockCount--;
292:
293: if (lockCount < 0) {
294: throw new JPFException("lock counter can't be negative");
295: }
296:
297: if (lockCount == 0) {
298: lockingThread = -1;
299: th.unlock(ref);
300: }
301: }
302:
303: /**
304: * Waits to be notified. Releases the lock and waits.
305: */
306: public void wait(ThreadInfo th, Ref ref) {
307: if (lockingThread != th.index) {
308: throw new JPFException("wait on an unlocked monitor");
309: }
310:
311: th.setStatus(ThreadInfo.WAITING);
312: th.setLockCount(lockCount);
313:
314: int length = waitingThreads.length;
315: int[] n = new int[length + 1];
316: System.arraycopy(waitingThreads, 0, n, 0, length);
317: waitingThreads = n;
318: waitingThreads[length] = th.index;
319:
320: lockingThread = -1;
321: lockCount = 0;
322:
323: th.unlock(ref);
324: }
325:
326: private int remove(int index) {
327: int r = waitingThreads[index];
328: int length = waitingThreads.length;
329:
330: int[] n = new int[length - 1];
331: System.arraycopy(waitingThreads, 0, n, 0, index);
332: System.arraycopy(waitingThreads, index + 1, n, index, length
333: - index - 1);
334: waitingThreads = n;
335:
336: return r;
337: }
338: }
|