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.Config;
022:
023: /**
024: * Contains the list of the threads
025: * It extends the storage interface.
026: */
027: public class ThreadList implements Storable {
028: /**
029: * The threads.
030: */
031: private ThreadInfo[] threads;
032:
033: /**
034: * Reference of the kernel state this thread list belongs to.
035: */
036: public KernelState ks;
037:
038: /**
039: * Creates a new empty thread list.
040: */
041: public ThreadList(Config config, KernelState ks) {
042: this .ks = ks;
043: threads = new ThreadInfo[0];
044: }
045:
046: public ThreadList(ThreadList tl) {
047: int l = tl.threads.length;
048: threads = new ThreadInfo[l];
049:
050: for (int i = 0; i < l; i++) {
051: threads[i] = (ThreadInfo) tl.threads[i].clone();
052: threads[i].list = this ;
053: threads[i].index = i;
054: }
055:
056: ks = null;
057: }
058:
059: /**
060: * Returns the data used for restoring the state.
061: */
062: public Object getBacktrackData() {
063: int length = threads.length;
064:
065: Object[] data = new Object[length];
066:
067: for (int i = 0; i < length; i++) {
068: if (threads[i] != null) {
069: data[i] = threads[i].getBacktrackData();
070: } else {
071: data[i] = null;
072: }
073: }
074:
075: return data;
076: }
077:
078: /**
079: * Returns the data used for storing the state.
080: */
081: public int[] getStoringData() {
082: int length = threads.length;
083:
084: int size = 0;
085: int[][] threadData = new int[length][];
086:
087: for (int i = 0; i < length; i++) {
088: if (threads[i] != null) {
089: size += (threadData[i] = threads[i].getStoringData()).length;
090: } else {
091: threadData[i] = null;
092: size++;
093: }
094: }
095:
096: int[] data = new int[size + 1];
097: data[0] = length;
098:
099: for (int i = 0, j = 1; i < length; i++) {
100: if (threadData[i] != null) {
101: int[] d = threadData[i];
102: int s = d.length;
103:
104: System.arraycopy(d, 0, data, j, s);
105: j += s;
106: } else {
107: data[j] = -1;
108: size++;
109: j++;
110: }
111: }
112:
113: return data;
114: }
115:
116: /**
117: * Adds a new thread to the list.
118: */
119: public void add(int index, ThreadInfo th) {
120: th.list = this ;
121: th.index = index;
122:
123: if (index >= threads.length) {
124: ThreadInfo[] n = new ThreadInfo[index + 1];
125: System.arraycopy(threads, 0, n, 0, threads.length);
126: threads = n;
127: }
128:
129: threads[index] = th;
130: ks.data = null;
131: }
132:
133: public boolean anyAliveThread() {
134: for (int i = 0, l = threads.length; i < l; i++) {
135: if (threads[i].isAlive()) {
136: return true;
137: }
138: }
139:
140: return false;
141: }
142:
143: /**
144: * Restores the state.
145: */
146: public void backtrackTo(ArrayOffset storing, Object backtrack) {
147: Object[] b = (Object[]) backtrack;
148:
149: int length = storing.get();
150: int l = threads.length;
151:
152: if (l != length) {
153: if (l > length) {
154: l = length;
155: }
156:
157: ThreadInfo[] n = new ThreadInfo[length];
158: System.arraycopy(threads, 0, n, 0, l);
159: threads = n;
160: }
161:
162: for (int i = 0; i < length; i++) {
163: ThreadInfo ti = threads[i];
164:
165: if (storing.peek() != -1) {
166: if (ti == null) {
167: ti = threads[i] = new ThreadInfo(this , i);
168: }
169:
170: ti.backtrackTo(storing, b[i]);
171: } else {
172: threads[i] = null;
173: storing.get();
174: }
175: }
176: }
177:
178: public Object clone() {
179: return new ThreadList(this );
180: }
181:
182: /**
183: * Returns a specific thread.
184: */
185: public ThreadInfo get(int index) {
186: return threads[index];
187: }
188:
189: /**
190: * Returns the length of the list.
191: */
192: public int length() {
193: return threads.length;
194: }
195:
196: public ThreadInfo locate(int objref) {
197: for (int i = 0, l = threads.length; i < l; i++) {
198: if (threads[i].getObjectReference() == objref) {
199: return threads[i];
200: }
201: }
202:
203: return null;
204: }
205:
206: public void markRoots() {
207: for (int i = 0, l = threads.length; i < l; i++) {
208: if (threads[i].isAlive()) {
209: threads[i].markRoots();
210: }
211: }
212: }
213:
214: public int getNonDaemonThreadCount() {
215: int nd = 0;
216:
217: for (int i = 0; i < threads.length; i++) {
218: if (!threads[i].isDaemon()) {
219: nd++;
220: }
221: }
222:
223: return nd;
224: }
225:
226: public int getRunnableThreadCount() {
227: int n = 0;
228:
229: for (int i = 0; i < threads.length; i++) {
230: if (threads[i].isRunnable()) {
231: n++;
232: }
233: }
234:
235: return n;
236: }
237:
238: boolean hasOtherRunnablesThan(int idx) {
239: int i;
240: int n = threads.length;
241:
242: for (i = 0; i < n; i++) {
243: if (i != idx) {
244: if (threads[i].isRunnable()) {
245: return true;
246: }
247: }
248: }
249:
250: return false;
251: }
252:
253: /**
254: * Removes a thread from the list.
255: */
256: public void remove(int index) {
257: threads[index].list = null;
258: threads[index].index = -1;
259: threads[index] = null;
260: ks.data = null;
261: }
262: }
|