[LLVMdev] More detailed example...

[Sarah Thompson]

Further to that, I thought an example might be useful. In the following 
code, n should end up with a value that varies nondeterministically with 
the scheduling decisions made by the underlying run time system -- my 
model checker, for example, should in theory be able to enumerate all 
possible values. Anyway, if you look at the compiler output (see below), 
the volatile global variable, n, has vanished, with the printf output 
only ever taking the (constant) result 0.

I somehow need to get around this, or my attempt to implement a C++ 
model checker is dead in the water.

Thank you in advance,
Sarah

PS: mcp_fork() duplicates the current stack as a new thread, and returns 
true within that thread and false in the original thread. mcp_yield() 
forces a reschedule. Stacks are separate, but the heap is shared. My 
model checker generates correct output for the generated code, but the 
generated code has the wrong semantics.

-----------------------------------------------------------------
Here is the test code:

#include <stdio.h>

#include "../../mcp/include/mcp.h"

volatile int n;
const int k = 3;

void inc(volatile int *p)
{
	int i;
	
	for(i=0; i<k; i++)
	{
		(*p)++;
		mcp_yield();
	}
}

void dec(volatile int *p)
{
	int i;
	
	for(i=0; i<k; i++)
	{
		(*p)--;
		mcp_yield();
	}
}

int main()
{
	n = 0;
	
	if(mcp_fork(1))
	{
		inc(&n);		
		return 0;
	}
	
	if(mcp_fork(2))
	{
		dec(&n);
		return 0;
	}
	
	printf("Result: n = %d\n", n);
	
	return 0;
}


---------------------------------------------------
llvm-dis output:

  ModuleID = 'incdec.bc'
target endian = little
target pointersize = 32
target triple = "i686-pc-linux-gnu"
deplibs = [ "stdc++", "c", "crtend" ]
%.str_1 = internal constant [16 x sbyte] c"Result: n = %d\0A\00"		; <[16 
x sbyte]*> [#uses=1]

implementation   ; Functions:

declare int %printf(sbyte*, ...)

declare void %mcp_yield()

int %main() {
entry:
	%tmp.0 = tail call bool %mcp_fork( ulong 1 )		; <bool> [#uses=1]
	br bool %tmp.0, label %_Z3incPVi.exit, label %endif.0

_Z3incPVi.exit:		; preds = %entry
	tail call void %mcp_yield( )
	tail call void %mcp_yield( )
	tail call void %mcp_yield( )
	ret int 0

endif.0:		; preds = %entry
	%tmp.1 = tail call bool %mcp_fork( ulong 2 )		; <bool> [#uses=1]
	br bool %tmp.1, label %_Z3decPVi.exit, label %endif.1

_Z3decPVi.exit:		; preds = %endif.0
	tail call void %mcp_yield( )
	tail call void %mcp_yield( )
	tail call void %mcp_yield( )
	ret int 0

endif.1:		; preds = %endif.0
	%tmp.2 = tail call int (sbyte*, ...)* %printf( sbyte* getelementptr 
([16 x sbyte]* %.str_1, int 0, int 0), int 0 )		; <int> [#uses=0]
	ret int 0
}

declare bool %mcp_fork(ulong)