2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.vm;
21 * a threshold FieldLockInfo with a set of lock candidates
23 * this is the destructive update version. Override singleLockThresholdFli() and lockSetthresholdFli() for
24 * a persistent version
26 public class LockSetThresholdFli extends ThresholdFieldLockInfo {
28 protected int[] lockRefSet;
30 // this is only used once during prototype generation
31 public LockSetThresholdFli(ThreadInfo ti, int[] currentLockRefs, int checkThreshold) {
32 super(checkThreshold);
35 lockRefSet = currentLockRefs;
39 protected int[] getCandidateLockSet() {
44 * override this for search global FieldLockInfos
46 protected SingleLockThresholdFli singleLockThresholdFli (ThreadInfo ti, int lockRef, int remainingChecks) {
47 return new SingleLockThresholdFli(ti, lockRef, remainingChecks);
50 protected LockSetThresholdFli lockSetThresholdFli (ThreadInfo ti, int[] lockRefs, int remainingChecks){
51 this.lockRefSet = lockRefs;
52 this.tiLastCheck = ti;
53 this.remainingChecks = remainingChecks;
59 public FieldLockInfo checkProtection(ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
60 int[] currentLockRefs = ti.getLockedObjectReferences();
61 int nLocks = currentLockRefs.length;
62 int nRemaining = Math.max(0, remainingChecks--);
64 if (nLocks == 0) { // no current locks, so intersection is empty
65 checkFailedLockAssumption(ti, ei, fi);
68 } else { // we had a lock set, and there currently is at least one lock held
70 int[] newLset = new int[lockRefSet.length];
72 for (int i = 0; i < nLocks; i++) { // get the set intersection
73 int leidx = currentLockRefs[i];
75 for (int j = 0; j < lockRefSet.length; j++) {
76 if (lockRefSet[j] == leidx) {
78 break; // sets don't contain duplicates
83 if (l == 0) { // intersection empty
84 checkFailedLockAssumption(ti, ei, fi);
87 } else if (l == 1) { // only one candidate left
88 return singleLockThresholdFli(ti, newLset[0], nRemaining);
90 } else if (l < newLset.length) { // candidate set did shrink
91 int[] newLockRefSet = new int[l];
92 System.arraycopy(newLset, 0, newLockRefSet, 0, l);
93 return lockSetThresholdFli(ti, newLockRefSet, nRemaining);
96 return lockSetThresholdFli(ti, lockRefSet, nRemaining);
102 * only called at the end of the gc on all live objects. The recycled ones are
103 * either already nulled in the heap, or are not marked as live
106 public FieldLockInfo cleanUp(Heap heap) {
110 if (lockRefSet != null) {
111 for (int i = 0; i < lockRefSet.length; i++) {
112 ElementInfo ei = heap.get(lockRefSet[i]);
114 if (!heap.isAlive(ei)) { // we got a stale one, so we have to change us
115 if (newSet == null) { // first one, copy everything up to it
116 newSet = new int[lockRefSet.length - 1];
118 System.arraycopy(lockRefSet, 0, newSet, 0, i);
124 if (newSet != null) { // we already had a dangling ref, now copy the live ones
125 newSet[l++] = lockRefSet[i];
132 assert (newSet != null);
133 return new SingleLockThresholdFli(tiLastCheck, newSet[0], remainingChecks);
136 if (newSet != null) {
137 if (l == newSet.length) { // we just had one stale ref
139 } else { // several stales - make a new copy
143 lockRefSet = new int[l];
144 System.arraycopy(newSet, 0, lockRefSet, 0, l);
153 public String toString() {
154 StringBuilder sb = new StringBuilder();
155 sb.append("LockSetThresholdFli {");
156 sb.append("remainingChecks=");
157 sb.append(remainingChecks);
158 sb.append(",lset=[");
159 if (lockRefSet != null) {
160 for (int i = 0; i < lockRefSet.length; i++) {
164 sb.append(lockRefSet[i]);
169 return sb.toString();