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