From: Mathieu Desnoyers Date: Wed, 14 Oct 2009 07:18:32 +0000 (-0400) Subject: add ticketlock test for wait-free (failed, as expected) X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=5c020b8d7d282dc5251caeb9fe5c4d1dd5be918c;p=userspace-rcu.git add ticketlock test for wait-free (failed, as expected) Signed-off-by: Mathieu Desnoyers --- diff --git a/ticketlock-testwait/DEFINES b/ticketlock-testwait/DEFINES new file mode 100644 index 0000000..4eb5315 --- /dev/null +++ b/ticketlock-testwait/DEFINES @@ -0,0 +1 @@ +#define refcount_gt_one (refcount > 1) diff --git a/ticketlock-testwait/Makefile b/ticketlock-testwait/Makefile new file mode 100644 index 0000000..c41afd3 --- /dev/null +++ b/ticketlock-testwait/Makefile @@ -0,0 +1,112 @@ +# 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 + +#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 diff --git a/ticketlock-testwait/asserts.log b/ticketlock-testwait/asserts.log new file mode 100644 index 0000000..1143d32 --- /dev/null +++ b/ticketlock-testwait/asserts.log @@ -0,0 +1,16 @@ +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' diff --git a/ticketlock-testwait/asserts.spin.input b/ticketlock-testwait/asserts.spin.input new file mode 100644 index 0000000..d2a22d2 --- /dev/null +++ b/ticketlock-testwait/asserts.spin.input @@ -0,0 +1,114 @@ +#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(); +} diff --git a/ticketlock-testwait/config_4_bits_per_byte.define b/ticketlock-testwait/config_4_bits_per_byte.define new file mode 100644 index 0000000..e1d13ca --- /dev/null +++ b/ticketlock-testwait/config_4_bits_per_byte.define @@ -0,0 +1 @@ +#define CONFIG_BITS_PER_BYTE 4 diff --git a/ticketlock-testwait/lock_progress.log b/ticketlock-testwait/lock_progress.log new file mode 100644 index 0000000..8ffef37 --- /dev/null +++ b/ticketlock-testwait/lock_progress.log @@ -0,0 +1,20 @@ +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) diff --git a/ticketlock-testwait/lock_progress.ltl b/ticketlock-testwait/lock_progress.ltl new file mode 100644 index 0000000..8718641 --- /dev/null +++ b/ticketlock-testwait/lock_progress.ltl @@ -0,0 +1 @@ +([] <> !np_) diff --git a/ticketlock-testwait/lock_progress.spin.input b/ticketlock-testwait/lock_progress.spin.input new file mode 100644 index 0000000..b7ce6a2 --- /dev/null +++ b/ticketlock-testwait/lock_progress.spin.input @@ -0,0 +1,130 @@ +#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(); +} diff --git a/ticketlock-testwait/lock_progress.spin.input.trail b/ticketlock-testwait/lock_progress.spin.input.trail new file mode 100644 index 0000000..c9c9642 --- /dev/null +++ b/ticketlock-testwait/lock_progress.spin.input.trail @@ -0,0 +1,3029 @@ +-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 diff --git a/ticketlock-testwait/lock_progress_4_bits_per_byte.log b/ticketlock-testwait/lock_progress_4_bits_per_byte.log new file mode 100644 index 0000000..5a62baf --- /dev/null +++ b/ticketlock-testwait/lock_progress_4_bits_per_byte.log @@ -0,0 +1,22 @@ +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' diff --git a/ticketlock-testwait/mem-progress.spin b/ticketlock-testwait/mem-progress.spin new file mode 100644 index 0000000..818f445 --- /dev/null +++ b/ticketlock-testwait/mem-progress.spin @@ -0,0 +1,129 @@ +/* + * 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(); +} diff --git a/ticketlock-testwait/mem.sh b/ticketlock-testwait/mem.sh new file mode 100644 index 0000000..56e8123 --- /dev/null +++ b/ticketlock-testwait/mem.sh @@ -0,0 +1,29 @@ +#!/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 +# Mathieu Desnoyers + +# Basic execution, without LTL clauses. See Makefile. + +spin -a mem.spin +cc -DSAFETY -o pan pan.c +./pan -v -c1 -X -m10000000 -w21 diff --git a/ticketlock-testwait/mem.spin b/ticketlock-testwait/mem.spin new file mode 100644 index 0000000..445ee9a --- /dev/null +++ b/ticketlock-testwait/mem.spin @@ -0,0 +1,83 @@ +/* + * 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(); +} diff --git a/ticketlock-testwait/refcount.log b/ticketlock-testwait/refcount.log new file mode 100644 index 0000000..ba8d94e --- /dev/null +++ b/ticketlock-testwait/refcount.log @@ -0,0 +1,18 @@ +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 diff --git a/ticketlock-testwait/refcount.ltl b/ticketlock-testwait/refcount.ltl new file mode 100644 index 0000000..48f971f --- /dev/null +++ b/ticketlock-testwait/refcount.ltl @@ -0,0 +1 @@ +[] (!(refcount_gt_one)) diff --git a/ticketlock-testwait/refcount.spin.input b/ticketlock-testwait/refcount.spin.input new file mode 100644 index 0000000..d2a22d2 --- /dev/null +++ b/ticketlock-testwait/refcount.spin.input @@ -0,0 +1,114 @@ +#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(); +} diff --git a/ticketlock-testwait/refcount_4_bits_per_byte.log b/ticketlock-testwait/refcount_4_bits_per_byte.log new file mode 100644 index 0000000..77fcc77 --- /dev/null +++ b/ticketlock-testwait/refcount_4_bits_per_byte.log @@ -0,0 +1,22 @@ +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' diff --git a/ticketlock-testwait/references.txt b/ticketlock-testwait/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/ticketlock-testwait/references.txt @@ -0,0 +1,7 @@ +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