llvm dev - Jan 2007 - [LLVMdev] More detailed example...

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)

Sarah Thompson wrote:
> 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.
How are you compiling this? I get the following sort of output:

void %inc(int* %p) {
entry:
        %tmp = volatile load int* %p            ; <int> [#uses=1]
        %tmp1 = add int %tmp, 1         ; <int> [#uses=1]
        volatile store int %tmp1, int* %p
        tail call void (...)* %mcp_yield( )
        %tmp.1 = volatile load int* %p          ; <int> [#uses=1]
        %tmp1.1 = add int %tmp.1, 1             ; <int> [#uses=1]
        volatile store int %tmp1.1, int* %p
        tail call void (...)* %mcp_yield( )
        %tmp.2 = volatile load int* %p          ; <int> [#uses=1]
        %tmp1.2 = add int %tmp.2, 1             ; <int> [#uses=1]
        volatile store int %tmp1.2, int* %p
        tail call void (...)* %mcp_yield( )
        ret void
}

I ran this with "llvm-gcc -c mcp.c -o mcp.bc". In the example you
gave,
 it is valid for LLVM to optimize away the volatile memory accesses if
it were doing link-time optimizations; it could prove that "int
n"'s
value never changed the observable behaviour of the program and elided it.

Nick Lewycky

On Fri, 5 Jan 2007, Nick Lewycky wrote:
> Sarah Thompson wrote:
>> 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.
>
> How are you compiling this? I get the following sort of output:
How are you compiling?  If you are running gccld, then your global is 
getting marked 'internal' and then the globalopt pass is promoting it to
a
local scalar.  We could make globalopt avoid doing this for globals with 
volatile accesses.

If you *are* running gccld, try passing -disable-internalize to see if 
this goes away.

-Chris

> void %inc(int* %p) {
> entry:
>        %tmp = volatile load int* %p            ; <int> [#uses=1]
>        %tmp1 = add int %tmp, 1         ; <int> [#uses=1]
>        volatile store int %tmp1, int* %p
>        tail call void (...)* %mcp_yield( )
>        %tmp.1 = volatile load int* %p          ; <int> [#uses=1]
>        %tmp1.1 = add int %tmp.1, 1             ; <int> [#uses=1]
>        volatile store int %tmp1.1, int* %p
>        tail call void (...)* %mcp_yield( )
>        %tmp.2 = volatile load int* %p          ; <int> [#uses=1]
>        %tmp1.2 = add int %tmp.2, 1             ; <int> [#uses=1]
>        volatile store int %tmp1.2, int* %p
>        tail call void (...)* %mcp_yield( )
>        ret void
> }
>
> I ran this with "llvm-gcc -c mcp.c -o mcp.bc". In the example you
gave,
> it is valid for LLVM to optimize away the volatile memory accesses if
> it were doing link-time optimizations; it could prove that "int
n"'s
> value never changed the observable behaviour of the program and elided it.
>
> Nick Lewycky
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
-Chris

-- 
http://nondot.org/sabre/
http://llvm.org/

> How are you compiling this? I get the following sort of output:
>
>   
llvm-gcc incdec.cpp -o incdec

I am currently using LLVM 1.8 -- I was basically holding off porting 
until LLVM 2.0 stabilises because I want to be able to move to 64 bit 
Intel and don't want to have to hit a moving target.
> void %inc(int* %p) {
> entry:
>         %tmp = volatile load int* %p            ; <int> [#uses=1]
>         %tmp1 = add int %tmp, 1         ; <int> [#uses=1]
>         volatile store int %tmp1, int* %p
>         tail call void (...)* %mcp_yield( )
>         %tmp.1 = volatile load int* %p          ; <int> [#uses=1]
>         %tmp1.1 = add int %tmp.1, 1             ; <int> [#uses=1]
>         volatile store int %tmp1.1, int* %p
>         tail call void (...)* %mcp_yield( )
>         %tmp.2 = volatile load int* %p          ; <int> [#uses=1]
>         %tmp1.2 = add int %tmp.2, 1             ; <int> [#uses=1]
>         volatile store int %tmp1.2, int* %p
>         tail call void (...)* %mcp_yield( )
>         ret void
> }
>
> I ran this with "llvm-gcc -c mcp.c -o mcp.bc". In the example you
gave,
>  it is valid for LLVM to optimize away the volatile memory accesses if
> it were doing link-time optimizations; it could prove that "int
n"'s
> value never changed the observable behaviour of the program and elided it.
>   
This looks right, and would definitely generate correct code if it was 
used. I will try again with the gcc command line you used.

Thanks,
Sarah