Spinroot

uh

Member

Registered: 2012-05-14

Posts: 2

Scheduling on Mac OS X (64-Bit) Snow Leopard

Hi,
   I installed spin as per installation instruction http://spinroot.com/spin/Man/README.html#2c
   on Max OS X.
   When I run the tests most of them run fine, but test 7 "check random number generator"
   seems to fail:

$ spin -p -g -u10000 priorities.pml
...
              2
9996:    proc  2 (A) priorities.pml:11 (state 3)    [printf('%d\\n',_pid)]
9997:    proc  0 (:init:) priorities.pml:20 (state 3)    <<Not Enabled>>
9997:    proc  2 (A) priorities.pml:12 (state 2)    [a[_pid] = (a[_pid]+1)]
        a[0] = 0
        a[1] = 0
        a[2] = 3332
        a[3] = 0
        a[4] = 0
9998:    proc  2 (A) priorities.pml:14 (state 4)    [.(goto)]
              2
9999:    proc  2 (A) priorities.pml:11 (state 3)    [printf('%d\\n',_pid)]
10000:    proc  1 (A) priorities.pml:11 (state 3)    <<Not Enabled>>
10000:    proc  2 (A) priorities.pml:12 (state 2)    [a[_pid] = (a[_pid]+1)]
        a[0] = 0
        a[1] = 0
        a[2] = 3333
        a[3] = 0
        a[4] = 0
-------------
depth-limit (-u10000 steps) reached
#processes: 3
        a[0] = 0
        a[1] = 0
        a[2] = 3333
        a[3] = 0
        a[4] = 0
10000:    proc  2 (A) priorities.pml:14 (state 4)
10000:    proc  1 (A) priorities.pml:11 (state 3)
10000:    proc  0 (:init:) priorities.pml:20 (state 3)
3 processes created

The expected result is that the counters in a should be in the ratio 1:2:3:4 (a[0] is expected to be 0).
It looks like the processes 1, 3 and 4 are never scheduled and process 2 runs all the time. Hmm.
How do I more closely test the random number generator?

This is Mac OS X 10.6.8
$ uname -a
Darwin uhoBookPro 10.8.0 Darwin Kernel Version 10.8.0: Tue Jun  7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386 i386

$ file spin
spin: Mach-O 64-bit executable x86_64

Any suggestions?

Regards,
       Ulrich Hoffmann

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Scheduling on Mac OS X (64-Bit) Snow Leopard

Yes the semantics of priorities has changed -- you should be able to get the old behavior with spin -o6
See the release notes for 6.2
I've fixed the README file to state this more clearly, for version 6.2.1

uh

Member

Registered: 2012-05-14

Posts: 2

Re: Scheduling on Mac OS X (64-Bit) Snow Leopard

Hi Spinroot, thanks for the quick answer. That helps a lot.

I did not yet complete wading the entire documentation :-)

Regards,
       Ulrich