Spinroot

feng_lei_76

Member

Registered: 2011-05-13

Posts: 43

My Problem with -DBFS_PAR

I have a simple model that works fine with normal -DBFS.  When I compile the file pan.c with -DBFS_PAR, the compilation is not successful with the message:

/cygdrive/c/Users/lfeng/AppData/Local/Temp/ccXcZ1QF.o: pan.c: <.text+0x2c42>: undefined reference to '__sync_bool_compare_and_swap'
collect2: ld returned 1 exit status

I'm using SPIN 621 on Windows 7, 64 bit and Cygwin.  The compiler is gcc-3.

Please help me identify the problem.  Thanks!

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: My Problem with -DBFS_PAR

try compiling with -DNO_CAS added as well
this avoids the use of that instruction

feng_lei_76

Member

Registered: 2011-05-13

Posts: 43

Re: My Problem with -DBFS_PAR

Yes, the compilation succeeded with the command
gcc-3 -O2 -DBFS_PAR -DNO_CAS -DSAFETY -DNOCLAIM -w -o pan pan.c

But after I typed "pan" in Windows Command Prompt.  Nothing appeared in the prompt.  The program finished without showing anything on the screen.

If I instead use -DBFS, pan works as expected.  What might be wrong?

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: My Problem with -DBFS_PAR

on what type of machine are you executing this?

the BFS_PAR algorithms have been tested most thoroughly on Ubuntu Linux (and should work the same on any Linux or Unix version).
Correct working has also been confirmed on 32-bit Windows with Cygwin
(not 64-bit Windows yet) -- but not much testing was done with Mac's or Sun/Solaris systems.

feng_lei_76

Member

Registered: 2011-05-13

Posts: 43

Re: My Problem with -DBFS_PAR

Oops.  My machine is out of the list.  It is a Dell laptop with 64 bit Windows 7 OS.  I should install a Linux virtual machine in my PC to further explore SPIN.  Thank you for the help!

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: My Problem with -DBFS_PAR

i'll do some experiments on a 64 bit Windows machine, and see if I can find out if it works correctly
part of the problem could be that cygwin has no support for 64-bit -- which means that you'd have to use the microsoft visual studio compilers

feng_lei_76

Member

Registered: 2011-05-13

Posts: 43

Re: My Problem with -DBFS_PAR

I made some tests with Microsoft Visual C++2010 Professional.  The pan.c file works fine with the conventional compiler options like SAFETY, NOCLAIM, and so on; however, as soon as I added the new options BFS_PAR and NO_CAS to enable parallel computing, the compilation failed.  The following is the error messages. 

1>ClCompile:
1>  pan.c
1>c:\users\lfeng\documents\spin\exercises\as1\pan.h(475): warning C4273: 'exit' : inconsistent dll linkage
1>          c:\Program Files (x86)\Microsoft Visual Studio 10.0\VC\include\stdlib.h(353) : see previous definition of 'exit'
1>..\..\pan.c(484): error C2054: expected '(' to follow 'inline'
1>..\..\pan.c(485): error C2085: 'bfs_prepmask' : not in formal parameter list
1>..\..\pan.c(485): error C2143: syntax error : missing ';' before '{'

After these lines there are tens of minor warning messages.  At the end is another error message.

1>c:\users\lfeng\documents\spin\exercises\as1\pan.p(1): fatal error C1083: Cannot open include file: 'sys/ipc.h': No such file or directory
1>
1>Build FAILED.

I hope my report may help you identify the sources.  For the time being, I'll continue to use SPIN via iSpin and cygwin.

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: My Problem with -DBFS_PAR

I just did a test with -DBFS_PAR, using a standard cygwin installation on a
64-bit  system with Windows 7 Home Premium.
My system has 64-bit Intel i5-2500 CPUs, quadcore.
If I compile (say leader.pml) with the cygwin gcc version, all goes well, but executing it fails with "bad system call".
This happens if you don't first start the cygserver for shared memory support.
You can find instructions for doing this at: http://spinroot.com/spin/multicore/setup.html -- look for the section titled:
"Setup for 32-bit Cygwin under Windows"
After you get the cygserver running, the executable works without problems.
So, I simply compiled with standard gcc to do this -- not with cl.  I think it's probably true that the new code for BFS_PAR isn't yet "cl-friendly" and tries to include standard linux/cygwin header files that microsoft visual studio doesn't like.