19 lines
		
	
	
		
			237 B
		
	
	
	
		
			Plaintext
		
	
	
	
	
	
			
		
		
	
	
			19 lines
		
	
	
		
			237 B
		
	
	
	
		
			Plaintext
		
	
	
	
	
	
| C CoWW+poonceonce
 | |
| 
 | |
| (*
 | |
|  * Result: Never
 | |
|  *
 | |
|  * Test of write-write coherence, that is, whether or not two successive
 | |
|  * writes to the same variable are ordered.
 | |
|  *)
 | |
| 
 | |
| {}
 | |
| 
 | |
| P0(int *x)
 | |
| {
 | |
| 	WRITE_ONCE(*x, 1);
 | |
| 	WRITE_ONCE(*x, 2);
 | |
| }
 | |
| 
 | |
| exists (x=1)
 |