--- /dev/null
+#define refcount_gt_one (refcount > 1)
--- /dev/null
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program; if not, write to the Free Software
+# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+#
+# Copyright (C) Mathieu Desnoyers, 2009
+#
+# Authors: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
+
+#CFLAGS=-DSAFETY
+#CFLAGS=-DHASH64 -DREACH
+CFLAGS=-DHASH64
+
+#try pan -i to get the smallest trace.
+
+SPINFILE=mem.spin
+SPINFILE_FAIR=mem-progress.spin
+
+default:
+ make refcount | tee refcount.log
+ make refcount_4_bits_per_byte | tee refcount_4_bits_per_byte.log
+ make lock_progress | tee lock_progress.log
+ make lock_progress_4_bits_per_byte | tee lock_progress_4_bits_per_byte.log
+ make asserts | tee asserts.log
+ make summary
+
+#show trail : spin -v -t -N pan.ltl input.spin
+# after each individual make.
+
+summary:
+ @echo
+ @echo "Verification summary"
+ @grep error *.log
+
+asserts: clean
+ cat DEFINES > .input.spin
+ cat ${SPINFILE} >> .input.spin
+ rm -f .input.spin.trail
+ spin -a -X .input.spin
+ gcc -w ${CFLAGS} -DSAFETY -o pan pan.c
+ ./pan -v -c1 -X -m10000000 -w19
+ cp .input.spin $@.spin.input
+ -cp .input.spin.trail $@.spin.input.trail
+
+refcount: clean refcount_ltl run
+ cp .input.spin $@.spin.input
+ -cp .input.spin.trail $@.spin.input.trail
+
+refcount_ltl:
+ touch .input.define
+ cat DEFINES > pan.ltl
+ cat .input.define >> pan.ltl
+ spin -f "!(`cat refcount.ltl | grep -v ^//`)" >> pan.ltl
+
+refcount_4_bits_per_byte: clean refcount_ltl config_4_bits_per_byte_define run
+
+lock_progress: clean lock_progress_ltl run_weak_fair
+ cp .input.spin $@.spin.input
+ -cp .input.spin.trail $@.spin.input.trail
+
+lock_progress_ltl:
+ touch .input.define
+ cat .input.define > pan.ltl
+ cat DEFINES >> pan.ltl
+ spin -f "!(`cat lock_progress.ltl | grep -v ^//`)" >> pan.ltl
+
+lock_progress_4_bits_per_byte: clean lock_progress_ltl config_4_bits_per_byte_define run
+
+config_4_bits_per_byte_define:
+ cp config_4_bits_per_byte.define .input.define
+
+run: pan
+ ./pan -a -v -c1 -X -m1000000 -w19
+
+run_weak_fair: pan_fair
+ ./pan_fair -a -f -v -c1 -X -m1000000 -w20
+
+pan_fair: pan_fair.c
+ gcc -w ${CFLAGS} -DNFAIR=4 -o pan_fair pan_fair.c
+
+pan: pan.c
+ gcc -w ${CFLAGS} -o pan pan.c
+
+pan_fair.c: pan.ltl ${SPINFILE_FAIR}
+ cat DEFINES > .input.spin
+ cat .input.define >> .input.spin
+ cat ${SPINFILE_FAIR} >> .input.spin
+ rm -f .input.spin.trail
+ spin -a -X -N pan.ltl .input.spin
+ mv pan.c pan_fair.c
+
+pan.c: pan.ltl ${SPINFILE}
+ cat DEFINES > .input.spin
+ cat .input.define >> .input.spin
+ cat ${SPINFILE} >> .input.spin
+ rm -f .input.spin.trail
+ spin -a -X -N pan.ltl .input.spin
+
+.PHONY: clean default distclean summary
+clean:
+ rm -f pan* trail.out .input.spin* *.spin.trail .input.define
+distclean:
+ rm -f *.trail *.input *.log
--- /dev/null
+make[1]: Entering directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
+rm -f pan* trail.out .input.spin* *.spin.trail .input.define
+cat DEFINES > .input.spin
+cat mem.spin >> .input.spin
+rm -f .input.spin.trail
+spin -a -X .input.spin
+spin: line 72 ".input.spin", Error: undeclared variable: do_pause saw ''(' = '40''
+spin: line 72 ".input.spin", Error: syntax error saw ''(' = '40''
+spin: line 86 ".input.spin", Error: bad call to proc_is_safe
+spin: line 86 ".input.spin", Error: bad call to proc_is_safe
+spin: line 86 ".input.spin", Error: bad call to proc_is_safe
+spin: line 86 ".input.spin", Error: bad call to proc_is_safe
+spin: line 86 ".input.spin", Error: bad call to proc_is_safe
+spin: line 80 ".input.spin", Error: proctype proc_X not found
+spin: 1 error(s) - aborting
+make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
--- /dev/null
+#define refcount_gt_one (refcount > 1)
+/*
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+ *
+ * Copyright (c) 2009 Mathieu Desnoyers
+ */
+
+/* 16 CPUs max (byte has 8 bits, divided in two) */
+
+#ifndef CONFIG_BITS_PER_BYTE
+#define BITS_PER_BYTE 8
+#else
+#define BITS_PER_BYTE CONFIG_BITS_PER_BYTE
+#endif
+
+#define HBPB (BITS_PER_BYTE / 2) /* 4 */
+#define HMASK ((1 << HBPB) - 1) /* 0x0F */
+
+/* for byte type */
+#define LOW_HALF(val) ((val) & HMASK)
+#define LOW_HALF_INC 1
+
+#define HIGH_HALF(val) ((val) & (HMASK << HBPB))
+#define HIGH_HALF_INC (1 << HBPB)
+
+byte lock = 0;
+byte refcount = 0;
+
+#define need_pause() (_pid == 1)
+
+/*
+ * Test weak fairness by either not pausing or cycling for any number of
+ * steps, or forever.
+ * Models a slow thread. Should be added between each atomic steps.
+ * To test for wait-freedom (no starvation of a specific thread), add do_pause
+ * in threads other than the one we are checking for progress (and which
+ * contains the progress label).
+ * To test for lock-freedom (system-wide progress), add to all threads except
+ * one. All threads contain progress labels.
+ */
+inline do_pause()
+{
+ if
+ :: need_pause() ->
+ do
+ :: 1 ->
+ if
+ :: 1 -> skip;
+ :: 1 -> break;
+ fi;
+ od;
+ :: else ->
+ skip;
+ fi;
+}
+
+inline spin_lock(lock, ticket)
+{
+ atomic {
+ ticket = HIGH_HALF(lock) >> HBPB;
+ lock = lock + HIGH_HALF_INC; /* overflow expected */
+ }
+
+ do
+ :: 1 ->
+ if
+ :: (LOW_HALF(lock) == ticket) ->
+ break;
+ :: else ->
+ skip;
+ fi;
+ od;
+}
+
+inline spin_unlock(lock)
+{
+ lock = HIGH_HALF(lock) | LOW_HALF(lock + LOW_HALF_INC);
+}
+
+proctype proc_X()
+{
+ byte ticket;
+
+ do
+ :: 1->
+ spin_lock(lock, ticket);
+progress:
+ refcount = refcount + 1;
+ do_pause();
+ refcount = refcount - 1;
+ spin_unlock(lock);
+ od;
+}
+
+init
+{
+ run proc_X();
+ run proc_X();
+ //run proc_X();
+ //run proc_X();
+ //run proc_X();
+}
--- /dev/null
+#define CONFIG_BITS_PER_BYTE 4
--- /dev/null
+make[1]: Entering directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
+rm -f pan* trail.out .input.spin* *.spin.trail .input.define
+touch .input.define
+cat .input.define > pan.ltl
+cat DEFINES >> pan.ltl
+spin -f "!(`cat lock_progress.ltl | grep -v ^//`)" >> pan.ltl
+cat DEFINES > .input.spin
+cat .input.define >> .input.spin
+cat mem-progress.spin >> .input.spin
+rm -f .input.spin.trail
+spin -a -X -N pan.ltl .input.spin
+Exit-Status 0
+mv pan.c pan_fair.c
+gcc -w -DHASH64 -DNFAIR=4 -o pan_fair pan_fair.c
+./pan_fair -a -f -v -c1 -X -m1000000 -w20
+warning: for p.o. reduction to be valid the never claim must be stutter-invariant
+(never claims generated from LTL formulae are stutter-invariant)
+depth 0: Claim reached state 5 (line 135)
+depth 2: Claim reached state 9 (line 140)
+depth 4992: Claim reached state 9 (line 139)
--- /dev/null
+([] <> !np_)
--- /dev/null
+#define refcount_gt_one (refcount > 1)
+/*
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+ *
+ * Copyright (c) 2009 Mathieu Desnoyers
+ */
+
+/* 16 CPUs max (byte has 8 bits, divided in two) */
+
+#ifndef CONFIG_BITS_PER_BYTE
+#define BITS_PER_BYTE 8
+#else
+// test progress failure with shorter byte size. Will fail with 5 proc.
+#define BITS_PER_BYTE CONFIG_BITS_PER_BYTE
+#endif
+
+#define HBPB (BITS_PER_BYTE / 2) /* 4 */
+#define HMASK ((1 << HBPB) - 1) /* 0x0F */
+
+/* for byte type */
+#define LOW_HALF(val) ((val) & HMASK)
+#define LOW_HALF_INC 1
+
+#define HIGH_HALF(val) ((val) & (HMASK << HBPB))
+#define HIGH_HALF_INC (1 << HBPB)
+
+byte lock = 0;
+byte refcount = 0;
+
+#define need_pause() (_pid == 2)
+
+/*
+ * Test weak fairness by either not pausing or cycling for any number of
+ * steps, or forever.
+ * Models a slow thread. Should be added between each atomic steps.
+ * To test for wait-freedom (no starvation of a specific thread), add do_pause
+ * in threads other than the one we are checking for progress (and which
+ * contains the progress label).
+ * To test for lock-freedom (system-wide progress), add to all threads except
+ * one. All threads contain progress labels.
+ */
+inline do_pause()
+{
+ if
+ :: need_pause() ->
+ if
+ :: 1 ->
+ do
+ :: 1 ->
+ skip;
+ od;
+ :: 1 -> skip;
+ fi;
+ :: else ->
+ skip;
+ fi;
+}
+
+inline spin_lock(lock, ticket)
+{
+ atomic {
+ ticket = HIGH_HALF(lock) >> HBPB;
+ lock = lock + HIGH_HALF_INC; /* overflow expected */
+ }
+
+ do
+ :: 1 ->
+ if
+ :: (LOW_HALF(lock) == ticket) ->
+ break;
+ :: else ->
+ skip;
+ fi;
+ od;
+}
+
+inline spin_unlock(lock)
+{
+ lock = HIGH_HALF(lock) | LOW_HALF(lock + LOW_HALF_INC);
+}
+
+proctype proc_A()
+{
+ byte ticket;
+
+ do
+ :: 1 ->
+progress_A:
+ spin_lock(lock, ticket);
+ refcount = refcount + 1;
+ refcount = refcount - 1;
+ spin_unlock(lock);
+ od;
+}
+
+proctype proc_B()
+{
+ byte ticket;
+
+ do
+ :: 1 ->
+ do_pause();
+ spin_lock(lock, ticket);
+ refcount = refcount + 1;
+ do_pause();
+ refcount = refcount - 1;
+ spin_unlock(lock);
+ od;
+}
+
+init
+{
+ run proc_A();
+ run proc_B();
+ run proc_B();
+ run proc_B();
+ run proc_B();
+}
--- /dev/null
+-2:3:-2
+-4:-4:-4
+1:0:86
+2:1:78
+3:0:86
+4:1:79
+5:0:86
+6:3:23
+7:0:86
+8:3:24
+9:0:86
+10:3:31
+11:0:86
+12:3:32
+13:0:86
+14:1:80
+15:0:86
+16:4:23
+17:0:86
+18:4:35
+19:0:86
+20:4:36
+21:0:86
+22:1:81
+23:0:86
+24:5:23
+25:0:86
+26:5:35
+27:0:86
+28:5:36
+29:0:86
+30:1:82
+31:0:86
+32:6:23
+33:0:86
+34:6:35
+35:0:86
+36:6:36
+37:0:86
+38:6:40
+39:0:86
+40:6:43
+41:0:86
+42:6:44
+43:0:86
+44:6:54
+45:0:86
+46:6:66
+47:0:86
+48:6:67
+49:0:86
+50:6:71
+51:0:86
+52:6:72
+53:0:86
+54:6:23
+55:0:86
+56:6:35
+57:0:86
+58:6:36
+59:0:86
+60:6:40
+61:0:86
+62:6:43
+63:0:86
+64:6:44
+65:0:86
+66:6:54
+67:0:86
+68:6:66
+69:0:86
+70:6:67
+71:0:86
+72:6:71
+73:0:86
+74:6:72
+75:0:86
+76:6:23
+77:0:86
+78:6:35
+79:0:86
+80:6:36
+81:0:86
+82:6:40
+83:0:86
+84:6:43
+85:0:86
+86:6:44
+87:0:86
+88:6:54
+89:0:86
+90:6:66
+91:0:86
+92:6:67
+93:0:86
+94:6:71
+95:0:86
+96:6:72
+97:0:86
+98:6:23
+99:0:86
+100:6:35
+101:0:86
+102:6:36
+103:0:86
+104:6:40
+105:0:86
+106:6:43
+107:0:86
+108:6:44
+109:0:86
+110:6:54
+111:0:86
+112:6:66
+113:0:86
+114:6:67
+115:0:86
+116:6:71
+117:0:86
+118:6:72
+119:0:86
+120:6:23
+121:0:86
+122:6:35
+123:0:86
+124:6:36
+125:0:86
+126:6:40
+127:0:86
+128:6:43
+129:0:86
+130:6:44
+131:0:86
+132:6:54
+133:0:86
+134:6:66
+135:0:86
+136:6:67
+137:0:86
+138:6:71
+139:0:86
+140:6:72
+141:0:86
+142:6:23
+143:0:86
+144:6:35
+145:0:86
+146:6:36
+147:0:86
+148:6:40
+149:0:86
+150:6:43
+151:0:86
+152:6:44
+153:0:86
+154:6:54
+155:0:86
+156:6:66
+157:0:86
+158:6:67
+159:0:86
+160:6:71
+161:0:86
+162:6:72
+163:0:86
+164:6:23
+165:0:86
+166:6:35
+167:0:86
+168:6:36
+169:0:86
+170:6:40
+171:0:86
+172:6:43
+173:0:86
+174:6:44
+175:0:86
+176:6:54
+177:0:86
+178:6:66
+179:0:86
+180:6:67
+181:0:86
+182:6:71
+183:0:86
+184:6:72
+185:0:86
+186:6:23
+187:0:86
+188:6:35
+189:0:86
+190:6:36
+191:0:86
+192:6:40
+193:0:86
+194:6:43
+195:0:86
+196:6:44
+197:0:86
+198:6:54
+199:0:86
+200:6:66
+201:0:86
+202:6:67
+203:0:86
+204:6:71
+205:0:86
+206:6:72
+207:0:86
+208:6:23
+209:0:86
+210:6:35
+211:0:86
+212:6:36
+213:0:86
+214:6:40
+215:0:86
+216:6:43
+217:0:86
+218:6:44
+219:0:86
+220:6:54
+221:0:86
+222:6:66
+223:0:86
+224:6:67
+225:0:86
+226:6:71
+227:0:86
+228:6:72
+229:0:86
+230:6:23
+231:0:86
+232:6:35
+233:0:86
+234:6:36
+235:0:86
+236:6:40
+237:0:86
+238:6:43
+239:0:86
+240:6:44
+241:0:86
+242:6:54
+243:0:86
+244:6:66
+245:0:86
+246:6:67
+247:0:86
+248:6:71
+249:0:86
+250:6:72
+251:0:86
+252:6:23
+253:0:86
+254:6:35
+255:0:86
+256:6:36
+257:0:86
+258:6:40
+259:0:86
+260:6:43
+261:0:86
+262:6:44
+263:0:86
+264:6:54
+265:0:86
+266:6:66
+267:0:86
+268:6:67
+269:0:86
+270:6:71
+271:0:86
+272:6:72
+273:0:86
+274:6:23
+275:0:86
+276:6:35
+277:0:86
+278:6:36
+279:0:86
+280:6:40
+281:0:86
+282:6:43
+283:0:86
+284:6:44
+285:0:86
+286:6:54
+287:0:86
+288:6:66
+289:0:86
+290:6:67
+291:0:86
+292:6:71
+293:0:86
+294:6:72
+295:0:86
+296:6:23
+297:0:86
+298:6:35
+299:0:86
+300:6:36
+301:0:86
+302:6:40
+303:0:86
+304:6:43
+305:0:86
+306:6:44
+307:0:86
+308:6:54
+309:0:86
+310:6:66
+311:0:86
+312:6:67
+313:0:86
+314:6:71
+315:0:86
+316:6:72
+317:0:86
+318:6:23
+319:0:86
+320:6:35
+321:0:86
+322:6:36
+323:0:86
+324:6:40
+325:0:86
+326:6:43
+327:0:86
+328:6:44
+329:0:86
+330:6:54
+331:0:86
+332:6:66
+333:0:86
+334:6:67
+335:0:86
+336:6:71
+337:0:86
+338:6:72
+339:0:86
+340:6:23
+341:0:86
+342:6:35
+343:0:86
+344:6:36
+345:0:86
+346:6:40
+347:0:86
+348:6:43
+349:0:86
+350:6:44
+351:0:86
+352:6:54
+353:0:86
+354:6:66
+355:0:86
+356:6:67
+357:0:86
+358:6:71
+359:0:86
+360:6:72
+361:0:86
+362:6:23
+363:0:86
+364:6:35
+365:0:86
+366:6:36
+367:0:86
+368:6:40
+369:0:86
+370:6:43
+371:0:86
+372:6:44
+373:0:86
+374:6:54
+375:0:86
+376:6:66
+377:0:86
+378:6:67
+379:0:86
+380:6:71
+381:0:86
+382:5:40
+383:0:86
+384:5:43
+385:0:86
+386:6:72
+387:0:86
+388:6:23
+389:0:86
+390:6:35
+391:0:86
+392:6:36
+393:0:86
+394:6:40
+395:0:86
+396:6:43
+397:0:86
+398:6:46
+399:0:86
+400:5:44
+401:0:86
+402:6:47
+403:0:86
+404:6:43
+405:0:86
+406:5:54
+407:0:86
+408:5:66
+409:0:86
+410:5:67
+411:0:86
+412:6:46
+413:0:86
+414:6:47
+415:0:86
+416:5:71
+417:0:86
+418:6:43
+419:0:86
+420:6:46
+421:0:86
+422:5:72
+423:0:86
+424:6:47
+425:0:86
+426:6:43
+427:0:86
+428:5:23
+429:0:86
+430:5:35
+431:0:86
+432:6:44
+433:0:86
+434:6:54
+435:0:86
+436:6:66
+437:0:86
+438:6:67
+439:0:86
+440:6:71
+441:0:86
+442:6:72
+443:0:86
+444:6:23
+445:0:86
+446:6:35
+447:0:86
+448:6:36
+449:0:86
+450:6:40
+451:0:86
+452:6:43
+453:0:86
+454:6:44
+455:0:86
+456:6:54
+457:0:86
+458:6:66
+459:0:86
+460:6:67
+461:0:86
+462:6:71
+463:0:86
+464:6:72
+465:0:86
+466:6:23
+467:0:86
+468:6:35
+469:0:86
+470:6:36
+471:0:86
+472:6:40
+473:0:86
+474:6:43
+475:0:86
+476:6:44
+477:0:86
+478:6:54
+479:0:86
+480:6:66
+481:0:86
+482:6:67
+483:0:86
+484:6:71
+485:0:86
+486:6:72
+487:0:86
+488:6:23
+489:0:86
+490:6:35
+491:0:86
+492:6:36
+493:0:86
+494:6:40
+495:0:86
+496:6:43
+497:0:86
+498:6:44
+499:0:86
+500:6:54
+501:0:86
+502:6:66
+503:0:86
+504:6:67
+505:0:86
+506:6:71
+507:0:86
+508:6:72
+509:0:86
+510:6:23
+511:0:86
+512:6:35
+513:0:86
+514:6:36
+515:0:86
+516:6:40
+517:0:86
+518:6:43
+519:0:86
+520:6:44
+521:0:86
+522:6:54
+523:0:86
+524:6:66
+525:0:86
+526:6:67
+527:0:86
+528:6:71
+529:0:86
+530:6:72
+531:0:86
+532:6:23
+533:0:86
+534:6:35
+535:0:86
+536:6:36
+537:0:86
+538:6:40
+539:0:86
+540:6:43
+541:0:86
+542:6:44
+543:0:86
+544:6:54
+545:0:86
+546:6:66
+547:0:86
+548:6:67
+549:0:86
+550:6:71
+551:0:86
+552:6:72
+553:0:86
+554:6:23
+555:0:86
+556:6:35
+557:0:86
+558:6:36
+559:0:86
+560:6:40
+561:0:86
+562:6:43
+563:0:86
+564:6:44
+565:0:86
+566:6:54
+567:0:86
+568:6:66
+569:0:86
+570:6:67
+571:0:86
+572:6:71
+573:0:86
+574:6:72
+575:0:86
+576:6:23
+577:0:86
+578:6:35
+579:0:86
+580:6:36
+581:0:86
+582:6:40
+583:0:86
+584:6:43
+585:0:86
+586:6:44
+587:0:86
+588:6:54
+589:0:86
+590:6:66
+591:0:86
+592:6:67
+593:0:86
+594:6:71
+595:0:86
+596:6:72
+597:0:86
+598:6:23
+599:0:86
+600:6:35
+601:0:86
+602:6:36
+603:0:86
+604:6:40
+605:0:86
+606:6:43
+607:0:86
+608:6:44
+609:0:86
+610:6:54
+611:0:86
+612:6:66
+613:0:86
+614:6:67
+615:0:86
+616:6:71
+617:0:86
+618:6:72
+619:0:86
+620:6:23
+621:0:86
+622:6:35
+623:0:86
+624:6:36
+625:0:86
+626:6:40
+627:0:86
+628:6:43
+629:0:86
+630:6:44
+631:0:86
+632:6:54
+633:0:86
+634:6:66
+635:0:86
+636:6:67
+637:0:86
+638:6:71
+639:0:86
+640:6:72
+641:0:86
+642:6:23
+643:0:86
+644:6:35
+645:0:86
+646:6:36
+647:0:86
+648:6:40
+649:0:86
+650:6:43
+651:0:86
+652:6:44
+653:0:86
+654:6:54
+655:0:86
+656:6:66
+657:0:86
+658:6:67
+659:0:86
+660:6:71
+661:0:86
+662:6:72
+663:0:86
+664:6:23
+665:0:86
+666:6:35
+667:0:86
+668:6:36
+669:0:86
+670:6:40
+671:0:86
+672:6:43
+673:0:86
+674:6:44
+675:0:86
+676:6:54
+677:0:86
+678:6:66
+679:0:86
+680:6:67
+681:0:86
+682:6:71
+683:0:86
+684:6:72
+685:0:86
+686:6:23
+687:0:86
+688:6:35
+689:0:86
+690:6:36
+691:0:86
+692:6:40
+693:0:86
+694:6:43
+695:0:86
+696:6:44
+697:0:86
+698:6:54
+699:0:86
+700:6:66
+701:0:86
+702:6:67
+703:0:86
+704:6:71
+705:0:86
+706:6:72
+707:0:86
+708:6:23
+709:0:86
+710:6:35
+711:0:86
+712:6:36
+713:0:86
+714:6:40
+715:0:86
+716:6:43
+717:0:86
+718:6:44
+719:0:86
+720:6:54
+721:0:86
+722:6:66
+723:0:86
+724:6:67
+725:0:86
+726:6:71
+727:0:86
+728:6:72
+729:0:86
+730:6:23
+731:0:86
+732:6:35
+733:0:86
+734:6:36
+735:0:86
+736:6:40
+737:0:86
+738:6:43
+739:0:86
+740:6:44
+741:0:86
+742:6:54
+743:0:86
+744:6:66
+745:0:86
+746:6:67
+747:0:86
+748:6:71
+749:0:86
+750:6:72
+751:0:86
+752:6:23
+753:0:86
+754:6:35
+755:0:86
+756:6:36
+757:0:86
+758:6:40
+759:0:86
+760:6:43
+761:0:86
+762:6:44
+763:0:86
+764:6:54
+765:0:86
+766:6:66
+767:0:86
+768:6:67
+769:0:86
+770:6:71
+771:0:86
+772:6:72
+773:0:86
+774:6:23
+775:0:86
+776:6:35
+777:0:86
+778:6:36
+779:0:86
+780:6:40
+781:0:86
+782:4:40
+783:0:86
+784:6:43
+785:0:86
+786:5:36
+787:0:86
+788:4:43
+789:0:86
+790:6:44
+791:0:86
+792:6:54
+793:0:86
+794:6:66
+795:0:86
+796:6:67
+797:0:86
+798:6:71
+799:0:86
+800:6:72
+801:0:86
+802:6:23
+803:0:86
+804:6:35
+805:0:86
+806:6:36
+807:0:86
+808:6:40
+809:0:86
+810:6:43
+811:0:86
+812:6:46
+813:0:86
+814:5:40
+815:0:86
+816:6:47
+817:0:86
+818:6:43
+819:0:86
+820:5:43
+821:0:86
+822:6:46
+823:0:86
+824:6:47
+825:0:86
+826:5:46
+827:0:86
+828:6:43
+829:0:86
+830:6:46
+831:0:86
+832:4:44
+833:0:86
+834:6:47
+835:0:86
+836:6:43
+837:0:86
+838:5:47
+839:0:86
+840:5:43
+841:0:86
+842:6:46
+843:0:86
+844:6:47
+845:0:86
+846:4:54
+847:0:86
+848:6:43
+849:0:86
+850:4:66
+851:0:86
+852:4:67
+853:0:86
+854:6:46
+855:0:86
+856:6:47
+857:0:86
+858:5:46
+859:0:86
+860:6:43
+861:0:86
+862:5:47
+863:0:86
+864:6:46
+865:0:86
+866:6:47
+867:0:86
+868:4:71
+869:0:86
+870:6:43
+871:0:86
+872:5:43
+873:0:86
+874:6:46
+875:0:86
+876:6:47
+877:0:86
+878:5:46
+879:0:86
+880:6:43
+881:0:86
+882:6:46
+883:0:86
+884:5:47
+885:0:86
+886:4:72
+887:0:86
+888:6:47
+889:0:86
+890:6:43
+891:0:86
+892:5:43
+893:0:86
+894:4:23
+895:0:86
+896:4:35
+897:0:86
+898:4:36
+899:0:86
+900:6:44
+901:0:86
+902:6:54
+903:0:86
+904:6:66
+905:0:86
+906:6:67
+907:0:86
+908:6:71
+909:0:86
+910:6:72
+911:0:86
+912:6:23
+913:0:86
+914:6:35
+915:0:86
+916:6:36
+917:0:86
+918:6:40
+919:0:86
+920:6:43
+921:0:86
+922:6:46
+923:0:86
+924:5:44
+925:0:86
+926:6:47
+927:0:86
+928:6:43
+929:0:86
+930:5:54
+931:0:86
+932:5:66
+933:0:86
+934:5:67
+935:0:86
+936:6:46
+937:0:86
+938:6:47
+939:0:86
+940:5:71
+941:0:86
+942:6:43
+943:0:86
+944:6:46
+945:0:86
+946:5:72
+947:0:86
+948:6:47
+949:0:86
+950:6:43
+951:0:86
+952:5:23
+953:0:86
+954:6:44
+955:0:86
+956:6:54
+957:0:86
+958:6:66
+959:0:86
+960:6:67
+961:0:86
+962:6:71
+963:0:86
+964:6:72
+965:0:86
+966:6:23
+967:0:86
+968:6:35
+969:0:86
+970:6:36
+971:0:86
+972:6:40
+973:0:86
+974:6:43
+975:0:86
+976:6:44
+977:0:86
+978:6:54
+979:0:86
+980:6:66
+981:0:86
+982:6:67
+983:0:86
+984:6:71
+985:0:86
+986:6:72
+987:0:86
+988:6:23
+989:0:86
+990:6:35
+991:0:86
+992:6:36
+993:0:86
+994:6:40
+995:0:86
+996:6:43
+997:0:86
+998:6:44
+999:0:86
+1000:6:54
+1001:0:86
+1002:6:66
+1003:0:86
+1004:6:67
+1005:0:86
+1006:6:71
+1007:0:86
+1008:6:72
+1009:0:86
+1010:6:23
+1011:0:86
+1012:6:35
+1013:0:86
+1014:6:36
+1015:0:86
+1016:6:40
+1017:0:86
+1018:6:43
+1019:0:86
+1020:6:44
+1021:0:86
+1022:6:54
+1023:0:86
+1024:6:66
+1025:0:86
+1026:6:67
+1027:0:86
+1028:6:71
+1029:0:86
+1030:6:72
+1031:0:86
+1032:6:23
+1033:0:86
+1034:6:35
+1035:0:86
+1036:6:36
+1037:0:86
+1038:6:40
+1039:0:86
+1040:6:43
+1041:0:86
+1042:6:44
+1043:0:86
+1044:6:54
+1045:0:86
+1046:6:66
+1047:0:86
+1048:6:67
+1049:0:86
+1050:6:71
+1051:0:86
+1052:6:72
+1053:0:86
+1054:6:23
+1055:0:86
+1056:6:35
+1057:0:86
+1058:6:36
+1059:0:86
+1060:6:40
+1061:0:86
+1062:6:43
+1063:0:86
+1064:6:44
+1065:0:86
+1066:6:54
+1067:0:86
+1068:6:66
+1069:0:86
+1070:6:67
+1071:0:86
+1072:6:71
+1073:0:86
+1074:6:72
+1075:0:86
+1076:6:23
+1077:0:86
+1078:6:35
+1079:0:86
+1080:6:36
+1081:0:86
+1082:6:40
+1083:0:86
+1084:6:43
+1085:0:86
+1086:6:44
+1087:0:86
+1088:6:54
+1089:0:86
+1090:6:66
+1091:0:86
+1092:6:67
+1093:0:86
+1094:6:71
+1095:0:86
+1096:6:72
+1097:0:86
+1098:6:23
+1099:0:86
+1100:6:35
+1101:0:86
+1102:6:36
+1103:0:86
+1104:6:40
+1105:0:86
+1106:6:43
+1107:0:86
+1108:6:44
+1109:0:86
+1110:6:54
+1111:0:86
+1112:6:66
+1113:0:86
+1114:6:67
+1115:0:86
+1116:6:71
+1117:0:86
+1118:6:72
+1119:0:86
+1120:6:23
+1121:0:86
+1122:6:35
+1123:0:86
+1124:6:36
+1125:0:86
+1126:6:40
+1127:0:86
+1128:6:43
+1129:0:86
+1130:6:44
+1131:0:86
+1132:6:54
+1133:0:86
+1134:6:66
+1135:0:86
+1136:6:67
+1137:0:86
+1138:6:71
+1139:0:86
+1140:6:72
+1141:0:86
+1142:6:23
+1143:0:86
+1144:6:35
+1145:0:86
+1146:6:36
+1147:0:86
+1148:6:40
+1149:0:86
+1150:6:43
+1151:0:86
+1152:6:44
+1153:0:86
+1154:6:54
+1155:0:86
+1156:6:66
+1157:0:86
+1158:6:67
+1159:0:86
+1160:6:71
+1161:0:86
+1162:6:72
+1163:0:86
+1164:6:23
+1165:0:86
+1166:6:35
+1167:0:86
+1168:6:36
+1169:0:86
+1170:6:40
+1171:0:86
+1172:6:43
+1173:0:86
+1174:6:44
+1175:0:86
+1176:6:54
+1177:0:86
+1178:6:66
+1179:0:86
+1180:6:67
+1181:0:86
+1182:6:71
+1183:0:86
+1184:6:72
+1185:0:86
+1186:6:23
+1187:0:86
+1188:6:35
+1189:0:86
+1190:6:36
+1191:0:86
+1192:6:40
+1193:0:86
+1194:6:43
+1195:0:86
+1196:6:44
+1197:0:86
+1198:6:54
+1199:0:86
+1200:6:66
+1201:0:86
+1202:6:67
+1203:0:86
+1204:6:71
+1205:0:86
+1206:6:72
+1207:0:86
+1208:6:23
+1209:0:86
+1210:6:35
+1211:0:86
+1212:6:36
+1213:0:86
+1214:6:40
+1215:0:86
+1216:4:40
+1217:0:86
+1218:6:43
+1219:0:86
+1220:6:44
+1221:0:86
+1222:5:35
+1223:0:86
+1224:5:36
+1225:0:86
+1226:6:54
+1227:0:86
+1228:6:66
+1229:0:86
+1230:6:67
+1231:0:86
+1232:6:71
+1233:0:86
+1234:6:72
+1235:0:86
+1236:6:23
+1237:0:86
+1238:6:35
+1239:0:86
+1240:6:36
+1241:0:86
+1242:6:40
+1243:0:86
+1244:6:43
+1245:0:86
+1246:6:46
+1247:0:86
+1248:5:40
+1249:0:86
+1250:6:47
+1251:0:86
+1252:6:43
+1253:0:86
+1254:5:43
+1255:0:86
+1256:6:46
+1257:0:86
+1258:6:47
+1259:0:86
+1260:5:46
+1261:0:86
+1262:6:43
+1263:0:86
+1264:6:46
+1265:0:86
+1266:3:40
+1267:0:86
+1268:6:47
+1269:0:86
+1270:6:43
+1271:0:86
+1272:5:47
+1273:0:86
+1274:5:43
+1275:0:86
+1276:4:43
+1277:0:86
+1278:3:43
+1279:0:86
+1280:6:46
+1281:0:86
+1282:6:47
+1283:0:86
+1284:5:46
+1285:0:86
+1286:6:43
+1287:0:86
+1288:5:47
+1289:0:86
+1290:6:46
+1291:0:86
+1292:6:47
+1293:0:86
+1294:4:44
+1295:0:86
+1296:6:43
+1297:0:86
+1298:5:43
+1299:0:86
+1300:6:46
+1301:0:86
+1302:6:47
+1303:0:86
+1304:5:46
+1305:0:86
+1306:6:43
+1307:0:86
+1308:6:46
+1309:0:86
+1310:5:47
+1311:0:86
+1312:4:54
+1313:0:86
+1314:6:47
+1315:0:86
+1316:6:43
+1317:0:86
+1318:5:43
+1319:0:86
+1320:4:66
+1321:0:86
+1322:4:67
+1323:0:86
+1324:6:46
+1325:0:86
+1326:6:47
+1327:0:86
+1328:5:46
+1329:0:86
+1330:6:43
+1331:0:86
+1332:5:47
+1333:0:86
+1334:6:46
+1335:0:86
+1336:6:47
+1337:0:86
+1338:4:71
+1339:0:86
+1340:6:43
+1341:0:86
+1342:5:43
+1343:0:86
+1344:6:46
+1345:0:86
+1346:6:47
+1347:0:86
+1348:5:46
+1349:0:86
+1350:6:43
+1351:0:86
+1352:6:46
+1353:0:86
+1354:5:47
+1355:0:86
+1356:4:72
+1357:0:86
+1358:6:47
+1359:0:86
+1360:6:43
+1361:0:86
+1362:5:43
+1363:0:86
+1364:4:23
+1365:0:86
+1366:4:35
+1367:0:86
+1368:4:36
+1369:0:86
+1370:6:44
+1371:0:86
+1372:6:54
+1373:0:86
+1374:6:66
+1375:0:86
+1376:6:67
+1377:0:86
+1378:6:71
+1379:0:86
+1380:6:72
+1381:0:86
+1382:6:23
+1383:0:86
+1384:6:35
+1385:0:86
+1386:6:36
+1387:0:86
+1388:6:40
+1389:0:86
+1390:6:43
+1391:0:86
+1392:6:46
+1393:0:86
+1394:5:44
+1395:0:86
+1396:6:47
+1397:0:86
+1398:6:43
+1399:0:86
+1400:5:54
+1401:0:86
+1402:5:66
+1403:0:86
+1404:5:67
+1405:0:86
+1406:6:46
+1407:0:86
+1408:6:47
+1409:0:86
+1410:5:71
+1411:0:86
+1412:6:43
+1413:0:86
+1414:6:46
+1415:0:86
+1416:5:72
+1417:0:86
+1418:6:47
+1419:0:86
+1420:6:43
+1421:0:86
+1422:5:23
+1423:0:86
+1424:5:35
+1425:0:86
+1426:5:36
+1427:0:86
+1428:6:46
+1429:0:86
+1430:6:47
+1431:0:86
+1432:5:40
+1433:0:86
+1434:6:43
+1435:0:86
+1436:5:43
+1437:0:86
+1438:6:46
+1439:0:86
+1440:6:47
+1441:0:86
+1442:5:46
+1443:0:86
+1444:6:43
+1445:0:86
+1446:6:46
+1447:0:86
+1448:5:47
+1449:0:86
+1450:4:40
+1451:0:86
+1452:6:47
+1453:0:86
+1454:6:43
+1455:0:86
+1456:5:43
+1457:0:86
+1458:4:43
+1459:0:86
+1460:6:46
+1461:0:86
+1462:6:47
+1463:0:86
+1464:5:46
+1465:0:86
+1466:6:43
+1467:0:86
+1468:5:47
+1469:0:86
+1470:6:46
+1471:0:86
+1472:6:47
+1473:0:86
+1474:4:46
+1475:0:86
+1476:6:43
+1477:0:86
+1478:5:43
+1479:0:86
+1480:6:46
+1481:0:86
+1482:6:47
+1483:0:86
+1484:5:46
+1485:0:86
+1486:6:43
+1487:0:86
+1488:6:46
+1489:0:86
+1490:5:47
+1491:0:86
+1492:3:44
+1493:0:86
+1494:6:47
+1495:0:86
+1496:6:43
+1497:0:86
+1498:5:43
+1499:0:86
+1500:4:47
+1501:0:86
+1502:4:43
+1503:0:86
+1504:6:46
+1505:0:86
+1506:6:47
+1507:0:86
+1508:5:46
+1509:0:86
+1510:6:43
+1511:0:86
+1512:5:47
+1513:0:86
+1514:6:46
+1515:0:86
+1516:6:47
+1517:0:86
+1518:3:54
+1519:0:86
+1520:6:43
+1521:0:86
+1522:5:43
+1523:0:86
+1524:3:55
+1525:0:86
+1526:3:56
+1527:0:86
+1528:3:57
+1529:0:86
+1530:6:46
+1531:0:86
+1532:6:47
+1533:0:86
+1534:5:46
+1535:0:86
+1536:6:43
+1537:0:86
+1538:5:47
+1539:0:86
+1540:6:46
+1541:0:86
+1542:6:47
+1543:0:86
+1544:4:46
+1545:0:86
+1546:6:43
+1547:0:86
+1548:5:43
+1549:0:86
+1550:4:47
+1551:0:86
+1552:6:46
+1553:0:86
+1554:6:47
+1555:0:86
+1556:5:46
+1557:0:86
+1558:6:43
+1559:0:86
+1560:5:47
+1561:0:86
+1562:6:46
+1563:0:86
+1564:6:47
+1565:0:86
+1566:3:58
+1567:0:86
+1568:6:43
+1569:0:86
+1570:5:43
+1571:0:86
+1572:6:46
+1573:0:86
+1574:6:47
+1575:0:86
+1576:5:46
+1577:0:86
+1578:6:43
+1579:0:86
+1580:6:46
+1581:0:86
+1582:5:47
+1583:0:86
+1584:4:43
+1585:0:86
+1586:6:47
+1587:0:86
+1588:6:43
+1589:0:86
+1590:4:46
+1591:0:86
+1592:5:43
+1593:0:86
+1594:6:46
+1595:0:86
+1596:6:47
+1597:0:86
+1598:5:46
+1599:0:86
+1600:6:43
+1601:0:86
+1602:6:46
+1603:0:86
+1604:5:47
+1605:0:86
+1606:6:47
+1607:0:86
+1608:2:0
+1609:0:86
+1610:6:43
+1611:0:86
+1612:5:43
+1613:0:86
+1614:4:47
+1615:0:86
+1616:4:43
+1617:0:86
+1618:3:57
+1619:0:86
+1620:6:46
+1621:0:86
+1622:6:47
+1623:0:86
+1624:5:46
+1625:0:86
+1626:6:43
+1627:0:86
+1628:5:47
+1629:0:86
+1630:6:46
+1631:0:86
+1632:6:47
+1633:0:86
+1634:4:46
+1635:0:86
+1636:6:43
+1637:0:86
+1638:5:43
+1639:0:86
+1640:4:47
+1641:0:86
+1642:6:46
+1643:0:86
+1644:6:47
+1645:0:86
+1646:5:46
+1647:0:86
+1648:6:43
+1649:0:86
+1650:5:47
+1651:0:86
+1652:6:46
+1653:0:86
+1654:6:47
+1655:0:86
+1656:3:58
+1657:0:86
+1658:6:43
+1659:0:86
+1660:6:46
+1661:0:86
+1662:5:43
+1663:0:86
+1664:6:47
+1665:0:86
+1666:5:46
+1667:0:86
+1668:6:43
+1669:0:86
+1670:6:46
+1671:0:86
+1672:4:43
+1673:0:86
+1674:6:47
+1675:0:86
+1676:6:43
+1677:0:86
+1678:5:47
+1679:0:86
+1680:6:46
+1681:0:86
+1682:6:47
+1683:0:86
+1684:5:43
+1685:0:86
+1686:4:46
+1687:0:86
+1688:5:46
+1689:0:86
+1690:6:43
+1691:0:86
+1692:6:46
+1693:0:86
+1694:5:47
+1695:0:86
+1696:5:43
+1697:0:86
+1698:3:57
+1699:0:86
+1700:6:47
+1701:0:86
+1702:5:46
+1703:0:86
+1704:6:43
+1705:0:86
+1706:6:46
+1707:0:86
+1708:5:47
+1709:0:86
+1710:2:1
+1711:0:84
+1712:6:47
+1713:0:90
+1714:6:43
+1715:0:90
+1716:5:43
+1717:0:90
+1718:4:47
+1719:0:90
+1720:4:43
+1721:0:90
+1722:3:58
+1723:0:90
+1724:3:57
+1725:0:90
+1726:6:46
+1727:0:90
+1728:6:47
+1729:0:90
+1730:5:46
+1731:0:90
+1732:6:43
+1733:0:90
+1734:5:47
+1735:0:90
+1736:6:46
+1737:0:90
+1738:6:47
+1739:0:90
+1740:4:46
+1741:0:90
+1742:6:43
+1743:0:90
+1744:5:43
+1745:0:90
+1746:4:47
+1747:0:90
+1748:6:46
+1749:0:90
+1750:6:47
+1751:0:90
+1752:5:46
+1753:0:90
+1754:6:43
+1755:0:90
+1756:5:47
+1757:0:90
+1758:6:46
+1759:0:90
+1760:6:47
+1761:0:90
+1762:3:58
+1763:0:90
+1764:6:43
+1765:0:90
+1766:5:43
+1767:0:90
+1768:6:46
+1769:0:90
+1770:6:47
+1771:0:90
+1772:5:46
+1773:0:90
+1774:6:43
+1775:0:90
+1776:6:46
+1777:0:90
+1778:5:47
+1779:0:90
+1780:4:43
+1781:0:90
+1782:6:47
+1783:0:90
+1784:6:43
+1785:0:90
+1786:4:46
+1787:0:90
+1788:5:43
+1789:0:90
+1790:6:46
+1791:0:90
+1792:6:47
+1793:0:90
+1794:5:46
+1795:0:90
+1796:6:43
+1797:0:90
+1798:6:46
+1799:0:90
+1800:5:47
+1801:0:90
+1802:6:47
+1803:0:90
+1804:2:4
+1805:0:90
+1806:6:43
+-1:-1:-1
+1807:0:90
+1808:5:43
+1809:0:90
+1810:4:47
+1811:0:90
+1812:4:43
+1813:0:90
+1814:3:57
+1815:0:90
+1816:6:46
+1817:0:90
+1818:6:47
+1819:0:90
+1820:5:46
+1821:0:90
+1822:6:43
+1823:0:90
+1824:5:47
+1825:0:90
+1826:6:46
+1827:0:90
+1828:6:47
+1829:0:90
+1830:4:46
+1831:0:90
+1832:6:43
+1833:0:90
+1834:5:43
+1835:0:90
+1836:4:47
+1837:0:90
+1838:6:46
+1839:0:90
+1840:6:47
+1841:0:90
+1842:5:46
+1843:0:90
+1844:6:43
+1845:0:90
+1846:5:47
+1847:0:90
+1848:6:46
+1849:0:90
+1850:6:47
+1851:0:90
+1852:3:58
+1853:0:90
+1854:6:43
+1855:0:90
+1856:6:46
+1857:0:90
+1858:5:43
+1859:0:90
+1860:6:47
+1861:0:90
+1862:5:46
+1863:0:90
+1864:6:43
+1865:0:90
+1866:6:46
+1867:0:90
+1868:4:43
+1869:0:90
+1870:6:47
+1871:0:90
+1872:6:43
+1873:0:90
+1874:5:47
+1875:0:90
+1876:6:46
+1877:0:90
+1878:6:47
+1879:0:90
+1880:5:43
+1881:0:90
+1882:4:46
+1883:0:90
+1884:5:46
+1885:0:90
+1886:6:43
+1887:0:90
+1888:6:46
+1889:0:90
+1890:5:47
+1891:0:90
+1892:5:43
+1893:0:90
+1894:3:57
+1895:0:90
+1896:6:47
+1897:0:90
+1898:5:46
+1899:0:90
+1900:6:43
+1901:0:90
+1902:6:46
+1903:0:90
+1904:5:47
+1905:0:90
+1906:2:7
+1907:0:90
+1908:6:47
+1909:0:90
+1910:6:43
+1911:0:90
+1912:5:43
+1913:0:90
+1914:4:47
+1915:0:90
+1916:4:43
+1917:0:90
+1918:3:58
+1919:0:90
+1920:6:46
+1921:0:90
+1922:6:47
+1923:0:90
+1924:5:46
+1925:0:90
+1926:6:43
+1927:0:90
+1928:5:47
+1929:0:90
+1930:6:46
+1931:0:90
+1932:6:47
+1933:0:90
+1934:4:46
+1935:0:90
+1936:6:43
+1937:0:90
+1938:5:43
+1939:0:90
+1940:4:47
+1941:0:90
+1942:6:46
+1943:0:90
+1944:6:47
+1945:0:90
+1946:5:46
+1947:0:90
+1948:6:43
+1949:0:90
+1950:5:47
+1951:0:90
+1952:6:46
+1953:0:90
+1954:6:47
+1955:0:90
+1956:3:57
+1957:0:90
+1958:6:43
+1959:0:90
+1960:6:46
+1961:0:90
+1962:5:43
+1963:0:90
+1964:6:47
+1965:0:90
+1966:5:46
+1967:0:90
+1968:6:43
+1969:0:90
+1970:6:46
+1971:0:90
+1972:4:43
+1973:0:90
+1974:6:47
+1975:0:90
+1976:6:43
+1977:0:90
+1978:5:47
+1979:0:90
+1980:6:46
+1981:0:90
+1982:6:47
+1983:0:90
+1984:5:43
+1985:0:90
+1986:4:46
+1987:0:90
+1988:5:46
+1989:0:90
+1990:6:43
+1991:0:90
+1992:6:46
+1993:0:90
+1994:3:58
+1995:0:90
+1996:6:47
+1997:0:90
+1998:6:43
+1999:0:90
+2000:2:8
+2001:0:90
+2002:5:47
+2003:0:90
+2004:5:43
+2005:0:90
+2006:4:47
+2007:0:90
+2008:4:43
+2009:0:90
+2010:3:57
+2011:0:90
+2012:6:46
+2013:0:90
+2014:6:47
+2015:0:90
+2016:5:46
+2017:0:90
+2018:6:43
+2019:0:90
+2020:5:47
+2021:0:90
+2022:6:46
+2023:0:90
+2024:6:47
+2025:0:90
+2026:4:46
+2027:0:90
+2028:6:43
+2029:0:90
+2030:5:43
+2031:0:90
+2032:4:47
+2033:0:90
+2034:6:46
+2035:0:90
+2036:6:47
+2037:0:90
+2038:5:46
+2039:0:90
+2040:6:43
+2041:0:90
+2042:5:47
+2043:0:90
+2044:6:46
+2045:0:90
+2046:6:47
+2047:0:90
+2048:3:58
+2049:0:90
+2050:6:43
+2051:0:90
+2052:6:46
+2053:0:90
+2054:5:43
+2055:0:90
+2056:6:47
+2057:0:90
+2058:5:46
+2059:0:90
+2060:6:43
+2061:0:90
+2062:6:46
+2063:0:90
+2064:4:43
+2065:0:90
+2066:6:47
+2067:0:90
+2068:6:43
+2069:0:90
+2070:5:47
+2071:0:90
+2072:6:46
+2073:0:90
+2074:6:47
+2075:0:90
+2076:5:43
+2077:0:90
+2078:4:46
+2079:0:90
+2080:5:46
+2081:0:90
+2082:5:47
+2083:0:90
+2084:6:43
+2085:0:90
+2086:5:43
+2087:0:90
+2088:4:47
+2089:0:90
+2090:4:43
+2091:0:90
+2092:3:57
+2093:0:90
+2094:6:46
+2095:0:90
+2096:6:47
+2097:0:90
+2098:6:43
+2099:0:90
+2100:3:58
+2101:0:90
+2102:6:46
+2103:0:90
+2104:6:47
+2105:0:90
+2106:5:46
+2107:0:90
+2108:6:43
+2109:0:90
+2110:5:47
+2111:0:90
+2112:5:43
+2113:0:90
+2114:3:57
+2115:0:90
+2116:6:46
+2117:0:90
+2118:6:47
+2119:0:90
+2120:5:46
+2121:0:90
+2122:6:43
+2123:0:90
+2124:5:47
+2125:0:90
+2126:6:46
+2127:0:90
+2128:6:47
+2129:0:90
+2130:4:46
+2131:0:90
+2132:6:43
+2133:0:90
+2134:5:43
+2135:0:90
+2136:6:46
+2137:0:90
+2138:6:47
+2139:0:90
+2140:5:46
+2141:0:90
+2142:6:43
+2143:0:90
+2144:6:46
+2145:0:90
+2146:5:47
+2147:0:90
+2148:4:47
+2149:0:90
+2150:6:47
+2151:0:90
+2152:6:43
+2153:0:90
+2154:4:43
+2155:0:90
+2156:6:46
+2157:0:90
+2158:6:47
+2159:0:90
+2160:5:43
+2161:0:90
+2162:5:46
+2163:0:90
+2164:6:43
+2165:0:90
+2166:6:46
+2167:0:90
+2168:2:4
+2169:0:90
+2170:6:47
+2171:0:90
+2172:6:43
+2173:0:90
+2174:5:47
+2175:0:90
+2176:5:43
+2177:0:90
+2178:3:58
+2179:0:90
+2180:3:57
+2181:0:90
+2182:6:46
+2183:0:90
+2184:6:47
+2185:0:90
+2186:5:46
+2187:0:90
+2188:6:43
+2189:0:90
+2190:5:47
+2191:0:90
+2192:6:46
+2193:0:90
+2194:6:47
+2195:0:90
+2196:4:46
+2197:0:90
+2198:6:43
+2199:0:90
+2200:5:43
+2201:0:90
+2202:4:47
+2203:0:90
+2204:6:46
+2205:0:90
+2206:6:47
+2207:0:90
+2208:5:46
+2209:0:90
+2210:6:43
+2211:0:90
+2212:5:47
+2213:0:90
+2214:6:46
+2215:0:90
+2216:6:47
+2217:0:90
+2218:3:58
+2219:0:90
+2220:6:43
+2221:0:90
+2222:5:43
+2223:0:90
+2224:6:46
+2225:0:90
+2226:6:47
+2227:0:90
+2228:5:46
+2229:0:90
+2230:6:43
+2231:0:90
+2232:6:46
+2233:0:90
+2234:5:47
+2235:0:90
+2236:4:43
+2237:0:90
+2238:6:47
+2239:0:90
+2240:6:43
+2241:0:90
+2242:4:46
+2243:0:90
+2244:5:43
+2245:0:90
+2246:6:46
+2247:0:90
+2248:6:47
+2249:0:90
+2250:2:7
+2251:0:90
+2252:6:43
+2253:0:90
+2254:4:47
+2255:0:90
+2256:4:43
+2257:0:90
+2258:3:57
+2259:0:90
+2260:6:46
+2261:0:90
+2262:6:47
+2263:0:90
+2264:6:43
+2265:0:90
+2266:3:58
+2267:0:90
+2268:6:46
+2269:0:90
+2270:6:47
+2271:0:90
+2272:5:46
+2273:0:90
+2274:6:43
+2275:0:90
+2276:5:47
+2277:0:90
+2278:5:43
+2279:0:90
+2280:3:57
+2281:0:90
+2282:6:46
+2283:0:90
+2284:6:47
+2285:0:90
+2286:5:46
+2287:0:90
+2288:6:43
+2289:0:90
+2290:5:47
+2291:0:90
+2292:6:46
+2293:0:90
+2294:6:47
+2295:0:90
+2296:4:46
+2297:0:90
+2298:6:43
+2299:0:90
+2300:5:43
+2301:0:90
+2302:4:47
+2303:0:90
+2304:4:43
+2305:0:90
+2306:3:58
+2307:0:90
+2308:3:57
+2309:0:90
+2310:6:46
+2311:0:90
+2312:6:47
+2313:0:90
+2314:5:46
+2315:0:90
+2316:6:43
+2317:0:90
+2318:5:47
+2319:0:90
+2320:6:46
+2321:0:90
+2322:6:47
+2323:0:90
+2324:4:46
+2325:0:90
+2326:6:43
+2327:0:90
+2328:5:43
+2329:0:90
+2330:4:47
+2331:0:90
+2332:6:46
+2333:0:90
+2334:6:47
+2335:0:90
+2336:5:46
+2337:0:90
+2338:6:43
+2339:0:90
+2340:5:47
+2341:0:90
+2342:6:46
+2343:0:90
+2344:6:47
+2345:0:90
+2346:3:58
+2347:0:90
+2348:6:43
+2349:0:90
+2350:5:43
+2351:0:90
+2352:6:46
+2353:0:90
+2354:6:47
+2355:0:90
+2356:5:46
+2357:0:90
+2358:6:43
+2359:0:90
+2360:6:46
+2361:0:90
+2362:5:47
+2363:0:90
+2364:4:43
+2365:0:90
+2366:6:47
+2367:0:90
+2368:6:43
+2369:0:90
+2370:4:46
+2371:0:90
+2372:5:43
+2373:0:90
+2374:6:46
+2375:0:90
+2376:6:47
+2377:0:90
+2378:5:46
+2379:0:90
+2380:6:43
+2381:0:90
+2382:6:46
+2383:0:90
+2384:3:57
+2385:0:90
+2386:6:47
+2387:0:90
+2388:6:43
+2389:0:90
+2390:2:8
+2391:0:90
+2392:6:46
+2393:0:90
+2394:6:47
+2395:0:90
+2396:6:43
+2397:0:90
+2398:5:47
+2399:0:90
+2400:5:43
+2401:0:90
+2402:4:47
+2403:0:90
+2404:6:46
+2405:0:90
+2406:6:47
+2407:0:90
+2408:6:43
+2409:0:90
+2410:5:46
+2411:0:90
+2412:5:47
+2413:0:90
+2414:5:43
+2415:0:90
+2416:6:46
+2417:0:90
+2418:6:47
+2419:0:90
+2420:5:46
+2421:0:90
+2422:5:47
+2423:0:90
+2424:3:58
+2425:0:90
+2426:6:43
+2427:0:90
+2428:5:43
+2429:0:90
+2430:4:43
+2431:0:90
+2432:6:46
+2433:0:90
+2434:6:47
+2435:0:90
+2436:5:46
+2437:0:90
+2438:6:43
+2439:0:90
+2440:5:47
+2441:0:90
+2442:6:46
+2443:0:90
+2444:6:47
+2445:0:90
+2446:4:46
+2447:0:90
+2448:6:43
+2449:0:90
+2450:5:43
+2451:0:90
+2452:4:47
+2453:0:90
+2454:6:46
+2455:0:90
+2456:6:47
+2457:0:90
+2458:5:46
+2459:0:90
+2460:6:43
+2461:0:90
+2462:5:47
+2463:0:90
+2464:6:46
+2465:0:90
+2466:6:47
+2467:0:90
+2468:2:4
+2469:0:90
+2470:6:43
+2471:0:90
+2472:5:43
+2473:0:90
+2474:4:43
+2475:0:90
+2476:6:46
+2477:0:90
+2478:6:47
+2479:0:90
+2480:5:46
+2481:0:90
+2482:6:43
+2483:0:90
+2484:5:47
+2485:0:90
+2486:6:46
+2487:0:90
+2488:6:47
+2489:0:90
+2490:4:46
+2491:0:90
+2492:6:43
+2493:0:90
+2494:5:43
+2495:0:90
+2496:6:46
+2497:0:90
+2498:6:47
+2499:0:90
+2500:5:46
+2501:0:90
+2502:6:43
+2503:0:90
+2504:6:46
+2505:0:90
+2506:5:47
+2507:0:90
+2508:4:47
+2509:0:90
+2510:5:43
+2511:0:90
+2512:6:47
+2513:0:90
+2514:5:46
+2515:0:90
+2516:6:43
+2517:0:90
+2518:6:46
+2519:0:90
+2520:4:43
+2521:0:90
+2522:2:7
+2523:0:90
+2524:6:47
+2525:0:90
+2526:6:43
+2527:0:90
+2528:5:47
+2529:0:90
+2530:5:43
+2531:0:90
+2532:6:46
+2533:0:90
+2534:6:47
+2535:0:90
+2536:4:46
+2537:0:90
+2538:6:43
+2539:0:90
+2540:4:47
+2541:0:90
+2542:6:46
+2543:0:90
+2544:6:47
+2545:0:90
+2546:5:46
+2547:0:90
+2548:6:43
+2549:0:90
+2550:5:47
+2551:0:90
+2552:6:46
+2553:0:90
+2554:6:47
+2555:0:90
+2556:4:43
+2557:0:90
+2558:4:46
+2559:0:90
+2560:6:43
+2561:0:90
+2562:6:46
+2563:0:90
+2564:5:43
+2565:0:90
+2566:5:46
+2567:0:90
+2568:6:47
+2569:0:90
+2570:6:43
+2571:0:90
+2572:2:8
+2573:0:90
+2574:6:46
+2575:0:90
+2576:6:47
+2577:0:90
+2578:3:57
+2579:0:90
+2580:6:43
+2581:0:90
+2582:6:46
+2583:0:90
+2584:4:47
+2585:0:90
+2586:4:43
+2587:0:90
+2588:2:4
+2589:0:90
+2590:6:47
+2591:0:90
+2592:6:43
+2593:0:90
+2594:6:46
+2595:0:90
+2596:5:47
+2597:0:90
+2598:6:47
+2599:0:90
+2600:6:43
+2601:0:90
+2602:5:43
+2603:0:90
+2604:6:46
+2605:0:90
+2606:6:47
+2607:0:90
+2608:5:46
+2609:0:90
+2610:6:43
+2611:0:90
+2612:6:46
+2613:0:90
+2614:4:46
+2615:0:90
+2616:6:47
+2617:0:90
+2618:6:43
+2619:0:90
+2620:5:47
+2621:0:90
+2622:6:46
+2623:0:90
+2624:5:43
+2625:0:90
+2626:6:47
+2627:0:90
+2628:6:43
+2629:0:90
+2630:4:47
+2631:0:90
+2632:6:46
+2633:0:90
+2634:6:47
+2635:0:90
+2636:5:46
+2637:0:90
+2638:6:43
+2639:0:90
+2640:5:47
+2641:0:90
+2642:6:46
+2643:0:90
+2644:6:47
+2645:0:90
+2646:4:43
+2647:0:90
+2648:6:43
+2649:0:90
+2650:6:46
+2651:0:90
+2652:5:43
+2653:0:90
+2654:6:47
+2655:0:90
+2656:6:43
+2657:0:90
+2658:5:46
+2659:0:90
+2660:6:46
+2661:0:90
+2662:3:58
+2663:0:90
+2664:6:47
+2665:0:90
+2666:6:43
+2667:0:90
+2668:5:47
+2669:0:90
+2670:6:46
+2671:0:90
+2672:6:47
+2673:0:90
+2674:5:43
+2675:0:90
+2676:6:43
+2677:0:90
+2678:4:46
+2679:0:90
+2680:6:46
+2681:0:90
+2682:6:47
+2683:0:90
+2684:5:46
+2685:0:90
+2686:6:43
+2687:0:90
+2688:6:46
+2689:0:90
+2690:5:47
+2691:0:90
+2692:6:47
+2693:0:90
+2694:4:47
+2695:0:90
+2696:6:43
+2697:0:90
+2698:6:46
+2699:0:90
+2700:5:43
+2701:0:90
+2702:6:47
+2703:0:90
+2704:6:43
+2705:0:90
+2706:5:46
+2707:0:90
+2708:6:46
+2709:0:90
+2710:3:57
+2711:0:90
+2712:6:47
+2713:0:90
+2714:6:43
+2715:0:90
+2716:5:47
+2717:0:90
+2718:6:46
+2719:0:90
+2720:6:47
+2721:0:90
+2722:5:43
+2723:0:90
+2724:6:43
+2725:0:90
+2726:4:43
+2727:0:90
+2728:6:46
+2729:0:90
+2730:6:47
+2731:0:90
+2732:5:46
+2733:0:90
+2734:6:43
+2735:0:90
+2736:6:46
+2737:0:90
+2738:5:47
+2739:0:90
+2740:6:47
+2741:0:90
+2742:6:43
+2743:0:90
+2744:4:46
+2745:0:90
+2746:6:46
+2747:0:90
+2748:5:43
+2749:0:90
+2750:6:47
+2751:0:90
+2752:5:46
+2753:0:90
+2754:6:43
+2755:0:90
+2756:6:46
+2757:0:90
+2758:2:7
+2759:0:90
+2760:6:47
+2761:0:90
+2762:6:43
+2763:0:90
+2764:5:47
+2765:0:90
+2766:5:43
+2767:0:90
+2768:4:47
+2769:0:90
+2770:6:46
+2771:0:90
+2772:6:47
+2773:0:90
+2774:5:46
+2775:0:90
+2776:6:43
+2777:0:90
+2778:6:46
+2779:0:90
+2780:5:47
+2781:0:90
+2782:6:47
+2783:0:90
+2784:6:43
+2785:0:90
+2786:4:43
+2787:0:90
+2788:6:46
+2789:0:90
+2790:6:47
+2791:0:90
+2792:5:43
+2793:0:90
+2794:6:43
+2795:0:90
+2796:3:58
+2797:0:90
+2798:6:46
+2799:0:90
+2800:6:47
+2801:0:90
+2802:5:46
+2803:0:90
+2804:6:43
+2805:0:90
+2806:6:46
+2807:0:90
+2808:5:47
+2809:0:90
+2810:6:47
+2811:0:90
+2812:6:43
+2813:0:90
+2814:4:46
+2815:0:90
+2816:6:46
+2817:0:90
+2818:6:47
+2819:0:90
+2820:5:43
+2821:0:90
+2822:6:43
+2823:0:90
+2824:6:46
+2825:0:90
+2826:5:46
+2827:0:90
+2828:6:47
+2829:0:90
+2830:6:43
+2831:0:90
+2832:4:47
+2833:0:90
+2834:6:46
+2835:0:90
+2836:5:47
+2837:0:90
+2838:6:47
+2839:0:90
+2840:6:43
+2841:0:90
+2842:5:43
+2843:0:90
+2844:6:46
+2845:0:90
+2846:6:47
+2847:0:90
+2848:2:8
+2849:0:90
+2850:6:43
+2851:0:90
+2852:5:46
+2853:0:90
+2854:6:46
+2855:0:90
+2856:5:47
+2857:0:90
+2858:6:47
+2859:0:90
+2860:6:43
+2861:0:90
+2862:4:43
+2863:0:90
+2864:6:46
+2865:0:90
+2866:6:47
+2867:0:90
+2868:5:43
+2869:0:90
+2870:6:43
+2871:0:90
+2872:5:46
+2873:0:90
+2874:4:46
+2875:0:90
+2876:6:46
+2877:0:90
+2878:6:47
+2879:0:90
+2880:5:47
+2881:0:90
+2882:6:43
+2883:0:90
+2884:5:43
+2885:0:90
+2886:6:46
+2887:0:90
+2888:6:47
+2889:0:90
+2890:3:57
+2891:0:90
+2892:6:43
+2893:0:90
+2894:5:46
+2895:0:90
+2896:6:46
+2897:0:90
+2898:6:47
+2899:0:90
+2900:4:47
+2901:0:90
+2902:6:43
+2903:0:90
+2904:6:46
+2905:0:90
+2906:5:47
+2907:0:90
+2908:6:47
+2909:0:90
+2910:6:43
+2911:0:90
+2912:5:43
+2913:0:90
+2914:6:46
+2915:0:90
+2916:6:47
+2917:0:90
+2918:4:43
+2919:0:90
+2920:6:43
+2921:0:90
+2922:5:46
+2923:0:90
+2924:6:46
+2925:0:90
+2926:5:47
+2927:0:90
+2928:6:47
+2929:0:90
+2930:6:43
+2931:0:90
+2932:2:4
+2933:0:90
+2934:6:46
+2935:0:90
+2936:6:47
+2937:0:90
+2938:5:43
+2939:0:90
+2940:6:43
+2941:0:90
+2942:6:46
+2943:0:90
+2944:5:46
+2945:0:90
+2946:6:47
+2947:0:90
+2948:6:43
+2949:0:90
+2950:4:46
+2951:0:90
+2952:6:46
+2953:0:90
+2954:5:47
+2955:0:90
+2956:6:47
+2957:0:90
+2958:6:43
+2959:0:90
+2960:5:43
+2961:0:90
+2962:4:47
+2963:0:90
+2964:6:46
+2965:0:90
+2966:6:47
+2967:0:90
+2968:5:46
+2969:0:90
+2970:6:43
+2971:0:90
+2972:5:47
+2973:0:90
+2974:6:46
+2975:0:90
+2976:6:47
+2977:0:90
+2978:3:58
+2979:0:90
+2980:6:43
+2981:0:90
+2982:6:46
+2983:0:90
+2984:5:43
+2985:0:90
+2986:6:47
+2987:0:90
+2988:6:43
+2989:0:90
+2990:5:46
+2991:0:90
+2992:6:46
+2993:0:90
+2994:4:43
+2995:0:90
+2996:6:47
+2997:0:90
+2998:6:43
+2999:0:90
+3000:5:47
+3001:0:90
+3002:6:46
+3003:0:90
+3004:6:47
+3005:0:90
+3006:5:43
+3007:0:90
+3008:6:43
+3009:0:90
+3010:4:46
+3011:0:90
+3012:6:46
+3013:0:90
+3014:6:47
+3015:0:90
+3016:5:46
+3017:0:90
+3018:6:43
+3019:0:90
+3020:6:46
+3021:0:90
+3022:5:47
+3023:0:90
+3024:6:47
+3025:0:90
+3026:6:43
--- /dev/null
+make[1]: Entering directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
+rm -f pan* trail.out .input.spin* *.spin.trail .input.define
+touch .input.define
+cat .input.define > pan.ltl
+cat DEFINES >> pan.ltl
+spin -f "!(`cat lock_progress.ltl | grep -v ^//`)" >> pan.ltl
+cp config_4_bits_per_byte.define .input.define
+cat DEFINES > .input.spin
+cat .input.define >> .input.spin
+cat mem.spin >> .input.spin
+rm -f .input.spin.trail
+spin -a -X -N pan.ltl .input.spin
+spin: line 73 "pan.___", Error: undeclared variable: do_pause saw ''(' = '40''
+spin: line 73 "pan.___", Error: syntax error saw ''(' = '40''
+spin: line 99 "pan.___", Error: bad call to proc_is_safe
+spin: line 99 "pan.___", Error: bad call to proc_is_safe
+spin: line 99 "pan.___", Error: bad call to proc_is_safe
+spin: line 99 "pan.___", Error: bad call to proc_is_safe
+spin: line 99 "pan.___", Error: bad call to proc_is_safe
+spin: line 81 "pan.___", Error: proctype proc_X not found
+spin: 1 error(s) - aborting
+make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
--- /dev/null
+/*
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+ *
+ * Copyright (c) 2009 Mathieu Desnoyers
+ */
+
+/* 16 CPUs max (byte has 8 bits, divided in two) */
+
+#ifndef CONFIG_BITS_PER_BYTE
+#define BITS_PER_BYTE 8
+#else
+// test progress failure with shorter byte size. Will fail with 5 proc.
+#define BITS_PER_BYTE CONFIG_BITS_PER_BYTE
+#endif
+
+#define HBPB (BITS_PER_BYTE / 2) /* 4 */
+#define HMASK ((1 << HBPB) - 1) /* 0x0F */
+
+/* for byte type */
+#define LOW_HALF(val) ((val) & HMASK)
+#define LOW_HALF_INC 1
+
+#define HIGH_HALF(val) ((val) & (HMASK << HBPB))
+#define HIGH_HALF_INC (1 << HBPB)
+
+byte lock = 0;
+byte refcount = 0;
+
+#define need_pause() (_pid == 2)
+
+/*
+ * Test weak fairness by either not pausing or cycling for any number of
+ * steps, or forever.
+ * Models a slow thread. Should be added between each atomic steps.
+ * To test for wait-freedom (no starvation of a specific thread), add do_pause
+ * in threads other than the one we are checking for progress (and which
+ * contains the progress label).
+ * To test for lock-freedom (system-wide progress), add to all threads except
+ * one. All threads contain progress labels.
+ */
+inline do_pause()
+{
+ if
+ :: need_pause() ->
+ if
+ :: 1 ->
+ do
+ :: 1 ->
+ skip;
+ od;
+ :: 1 -> skip;
+ fi;
+ :: else ->
+ skip;
+ fi;
+}
+
+inline spin_lock(lock, ticket)
+{
+ atomic {
+ ticket = HIGH_HALF(lock) >> HBPB;
+ lock = lock + HIGH_HALF_INC; /* overflow expected */
+ }
+
+ do
+ :: 1 ->
+ if
+ :: (LOW_HALF(lock) == ticket) ->
+ break;
+ :: else ->
+ skip;
+ fi;
+ od;
+}
+
+inline spin_unlock(lock)
+{
+ lock = HIGH_HALF(lock) | LOW_HALF(lock + LOW_HALF_INC);
+}
+
+proctype proc_A()
+{
+ byte ticket;
+
+ do
+ :: 1 ->
+progress_A:
+ spin_lock(lock, ticket);
+ refcount = refcount + 1;
+ refcount = refcount - 1;
+ spin_unlock(lock);
+ od;
+}
+
+proctype proc_B()
+{
+ byte ticket;
+
+ do
+ :: 1 ->
+ do_pause();
+ spin_lock(lock, ticket);
+ refcount = refcount + 1;
+ do_pause();
+ refcount = refcount - 1;
+ spin_unlock(lock);
+ od;
+}
+
+init
+{
+ run proc_A();
+ run proc_B();
+ run proc_B();
+ run proc_B();
+ run proc_B();
+}
--- /dev/null
+#!/bin/sh
+#
+# Compiles and runs the urcu.spin Promela model.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program; if not, write to the Free Software
+# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+#
+# Copyright (C) IBM Corporation, 2009
+# Mathieu Desnoyers, 2009
+#
+# Authors: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
+# Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
+
+# Basic execution, without LTL clauses. See Makefile.
+
+spin -a mem.spin
+cc -DSAFETY -o pan pan.c
+./pan -v -c1 -X -m10000000 -w21
--- /dev/null
+/*
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+ *
+ * Copyright (c) 2009 Mathieu Desnoyers
+ */
+
+/* 16 CPUs max (byte has 8 bits, divided in two) */
+
+#ifndef CONFIG_BITS_PER_BYTE
+#define BITS_PER_BYTE 8
+#else
+#define BITS_PER_BYTE CONFIG_BITS_PER_BYTE
+#endif
+
+#define HBPB (BITS_PER_BYTE / 2) /* 4 */
+#define HMASK ((1 << HBPB) - 1) /* 0x0F */
+
+/* for byte type */
+#define LOW_HALF(val) ((val) & HMASK)
+#define LOW_HALF_INC 1
+
+#define HIGH_HALF(val) ((val) & (HMASK << HBPB))
+#define HIGH_HALF_INC (1 << HBPB)
+
+byte lock = 0;
+byte refcount = 0;
+
+inline spin_lock(lock, ticket)
+{
+ atomic {
+ ticket = HIGH_HALF(lock) >> HBPB;
+ lock = lock + HIGH_HALF_INC; /* overflow expected */
+ }
+
+ do
+ :: 1 ->
+ if
+ :: (LOW_HALF(lock) == ticket) ->
+ break;
+ :: else ->
+ skip;
+ fi;
+ od;
+}
+
+inline spin_unlock(lock)
+{
+ lock = HIGH_HALF(lock) | LOW_HALF(lock + LOW_HALF_INC);
+}
+
+proctype proc_X()
+{
+ byte ticket;
+
+ do
+ :: 1->
+ spin_lock(lock, ticket);
+ refcount = refcount + 1;
+ refcount = refcount - 1;
+ spin_unlock(lock);
+ od;
+}
+
+init
+{
+ run proc_X();
+ run proc_X();
+ run proc_X();
+ run proc_X();
+ run proc_X();
+}
--- /dev/null
+make[1]: Entering directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
+rm -f pan* trail.out .input.spin* *.spin.trail .input.define
+touch .input.define
+cat DEFINES > pan.ltl
+cat .input.define >> pan.ltl
+spin -f "!(`cat refcount.ltl | grep -v ^//`)" >> pan.ltl
+cat DEFINES > .input.spin
+cat .input.define >> .input.spin
+cat mem.spin >> .input.spin
+rm -f .input.spin.trail
+spin -a -X -N pan.ltl .input.spin
+Exit-Status 0
+gcc -w -DHASH64 -o pan pan.c
+./pan -a -v -c1 -X -m1000000 -w19
+warning: for p.o. reduction to be valid the never claim must be stutter-invariant
+(never claims generated from LTL formulae are stutter-invariant)
+depth 0: Claim reached state 5 (line 89)
+Depth= 889941 States= 1e+06 Transitions= 2.5e+06 Memory= 103.585 t= 3.39 R= 3e+05
--- /dev/null
+[] (!(refcount_gt_one))
--- /dev/null
+#define refcount_gt_one (refcount > 1)
+/*
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 2 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+ *
+ * Copyright (c) 2009 Mathieu Desnoyers
+ */
+
+/* 16 CPUs max (byte has 8 bits, divided in two) */
+
+#ifndef CONFIG_BITS_PER_BYTE
+#define BITS_PER_BYTE 8
+#else
+#define BITS_PER_BYTE CONFIG_BITS_PER_BYTE
+#endif
+
+#define HBPB (BITS_PER_BYTE / 2) /* 4 */
+#define HMASK ((1 << HBPB) - 1) /* 0x0F */
+
+/* for byte type */
+#define LOW_HALF(val) ((val) & HMASK)
+#define LOW_HALF_INC 1
+
+#define HIGH_HALF(val) ((val) & (HMASK << HBPB))
+#define HIGH_HALF_INC (1 << HBPB)
+
+byte lock = 0;
+byte refcount = 0;
+
+#define need_pause() (_pid == 1)
+
+/*
+ * Test weak fairness by either not pausing or cycling for any number of
+ * steps, or forever.
+ * Models a slow thread. Should be added between each atomic steps.
+ * To test for wait-freedom (no starvation of a specific thread), add do_pause
+ * in threads other than the one we are checking for progress (and which
+ * contains the progress label).
+ * To test for lock-freedom (system-wide progress), add to all threads except
+ * one. All threads contain progress labels.
+ */
+inline do_pause()
+{
+ if
+ :: need_pause() ->
+ do
+ :: 1 ->
+ if
+ :: 1 -> skip;
+ :: 1 -> break;
+ fi;
+ od;
+ :: else ->
+ skip;
+ fi;
+}
+
+inline spin_lock(lock, ticket)
+{
+ atomic {
+ ticket = HIGH_HALF(lock) >> HBPB;
+ lock = lock + HIGH_HALF_INC; /* overflow expected */
+ }
+
+ do
+ :: 1 ->
+ if
+ :: (LOW_HALF(lock) == ticket) ->
+ break;
+ :: else ->
+ skip;
+ fi;
+ od;
+}
+
+inline spin_unlock(lock)
+{
+ lock = HIGH_HALF(lock) | LOW_HALF(lock + LOW_HALF_INC);
+}
+
+proctype proc_X()
+{
+ byte ticket;
+
+ do
+ :: 1->
+ spin_lock(lock, ticket);
+progress:
+ refcount = refcount + 1;
+ do_pause();
+ refcount = refcount - 1;
+ spin_unlock(lock);
+ od;
+}
+
+init
+{
+ run proc_X();
+ run proc_X();
+ //run proc_X();
+ //run proc_X();
+ //run proc_X();
+}
--- /dev/null
+make[1]: Entering directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
+rm -f pan* trail.out .input.spin* *.spin.trail .input.define
+touch .input.define
+cat DEFINES > pan.ltl
+cat .input.define >> pan.ltl
+spin -f "!(`cat refcount.ltl | grep -v ^//`)" >> pan.ltl
+cp config_4_bits_per_byte.define .input.define
+cat DEFINES > .input.spin
+cat .input.define >> .input.spin
+cat mem.spin >> .input.spin
+rm -f .input.spin.trail
+spin -a -X -N pan.ltl .input.spin
+spin: line 73 "pan.___", Error: undeclared variable: do_pause saw ''(' = '40''
+spin: line 73 "pan.___", Error: syntax error saw ''(' = '40''
+spin: line 97 "pan.___", Error: bad call to proc_is_safe
+spin: line 97 "pan.___", Error: bad call to proc_is_safe
+spin: line 97 "pan.___", Error: bad call to proc_is_safe
+spin: line 97 "pan.___", Error: bad call to proc_is_safe
+spin: line 97 "pan.___", Error: bad call to proc_is_safe
+spin: line 81 "pan.___", Error: proctype proc_X not found
+spin: 1 error(s) - aborting
+make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
--- /dev/null
+http://spinroot.com/spin/Man/ltl.html
+http://en.wikipedia.org/wiki/Linear_temporal_logic
+http://www.dcs.gla.ac.uk/~muffy/MRS4-2002/lect11.ppt
+
+http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php
+http://spinroot.com/spin/Man/index.html
+http://spinroot.com/spin/Man/promela.html
projects / userspace-rcu.git / commitdiff
