My favorites | Sign in
Logo
                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
/**
* Copyright (C) 2007, 2008 Carnegie Mellon University and others.
*
* This file is part of Plural.
*
* Plural is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License version 2 as
* published by the Free Software Foundation.
*
* Plural is distributed in the hope that it will be useful, but
* WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with Plural; if not, see <http://www.gnu.org/licenses>.
*
* Linking Plural statically or dynamically with other modules is
* making a combined work based on Plural. Thus, the terms and
* conditions of the GNU General Public License cover the whole
* combination.
*
* In addition, as a special exception, the copyright holders of Plural
* give you permission to combine Plural with free software programs or
* libraries that are released under the GNU LGPL and with code
* included in the standard release of Eclipse under the Eclipse Public
* License (or modified versions of such code, with unchanged license).
* You may copy and distribute such a system following the terms of the
* GNU GPL for Plural and the licenses of the other code concerned.
*
* Note that people who make modified versions of Plural are not
* obligated to grant this special exception for their modified
* versions; it is their choice whether to do so. The GNU General
* Public License gives permission to release a modified version
* without this exception; this exception also makes it possible to
* release a modified version which carries forward this exception.
*/

package edu.cmu.cs.nimby.test.interesting;
import com.holub.asynch.Blocking_queue;

import edu.cmu.cs.crystal.annotations.PassingTest;
import edu.cmu.cs.crystal.annotations.UseAnalyses;
import edu.cmu.cs.plural.annot.ClassStates;
import edu.cmu.cs.plural.annot.Perm;
import edu.cmu.cs.plural.annot.PluralAnalysis;
import edu.cmu.cs.plural.annot.State;
import edu.cmu.cs.plural.annot.Unique;
import edu.cmu.cs.plural.annot.Use;


@PassingTest
@UseAnalyses(PluralAnalysis.NIMBY)
public class OneReaderOneWrtier {

public static void main(String[] args) {

Blocking_queue queue = new Blocking_queue();

(new Reader(queue)).start();

for(int i = 0;i<5;i++) {
queue.enqueue("OBJECT: " + i);
}

queue.close();
}

@ClassStates(@State(name="alive",
inv="pure(queue,PROTOCOL) * share(queue,STRUCTURE)"))
public static class Reader extends Thread {

private final Blocking_queue queue;

@Perm(requires="pure(#0,PROTOCOL) * share(#0,STRUCTURE)",
ensures="unique(this!fr)")
public Reader(Blocking_queue queue) {
this.queue = queue;
}

@Override
@Unique(use = Use.FIELDS)
public void run() {

boolean was_closed = false;
do {
Object obj = null;
atomic: {
was_closed = queue.is_closed();

if( !was_closed ) {
try{obj = queue.dequeue();}
catch(InterruptedException e){}
// NEB: Won't be necessary once we're using retry
}
else {
obj = null;
}
}
System.out.println("Got item: " + obj);
} while(!was_closed);

}

@Override
@Unique(returned=false)
public synchronized void start() {
super.start();
}
}

}
Show details Hide details

Change log

r264 by kevin.bierhoff on Mar 26, 2009   Diff
Port to new "use" attribute, replacing
fieldAccess flag
Go to: 
Project members, sign in to write a code review

Older revisions

r188 by nels.beckman on Dec 08, 2008   Diff
Finally got the blocking queue as a
real regression test.
r128 by nels.beckman on Oct 21, 2008   Diff
Adding some notes about copyright and
permission.
r127 by nels.beckman on Oct 21, 2008   Diff
Committing Blocking queue so that if
people from OOPSLA want to see it they
can. I have not annotated the files
with the testing annotations b/c I
cannot run the tests on this machine.
...
All revisions of this file

File info

Size: 3556 bytes, 112 lines
Hosted by Google Code