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();
		}
	}
	
}