From: Mathieu Desnoyers Date: Wed, 14 Oct 2009 22:20:49 +0000 (-0400) Subject: update X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=307daf8c9b05b394c48c069083891d6dc14ff345;p=urcu.git update Signed-off-by: Mathieu Desnoyers --- diff --git a/ticketlock-testwait/asserts.log b/ticketlock-testwait/asserts.log deleted file mode 100644 index 1143d32..0000000 --- a/ticketlock-testwait/asserts.log +++ /dev/null @@ -1,16 +0,0 @@ -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 deleted file mode 100644 index d2a22d2..0000000 --- a/ticketlock-testwait/asserts.spin.input +++ /dev/null @@ -1,114 +0,0 @@ -#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/lock_progress.log b/ticketlock-testwait/lock_progress.log deleted file mode 100644 index 8ffef37..0000000 --- a/ticketlock-testwait/lock_progress.log +++ /dev/null @@ -1,20 +0,0 @@ -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.spin.input b/ticketlock-testwait/lock_progress.spin.input deleted file mode 100644 index b7ce6a2..0000000 --- a/ticketlock-testwait/lock_progress.spin.input +++ /dev/null @@ -1,130 +0,0 @@ -#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 deleted file mode 100644 index c9c9642..0000000 --- a/ticketlock-testwait/lock_progress.spin.input.trail +++ /dev/null @@ -1,3029 +0,0 @@ --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 deleted file mode 100644 index 5a62baf..0000000 --- a/ticketlock-testwait/lock_progress_4_bits_per_byte.log +++ /dev/null @@ -1,22 +0,0 @@ -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/refcount.log b/ticketlock-testwait/refcount.log deleted file mode 100644 index ba8d94e..0000000 --- a/ticketlock-testwait/refcount.log +++ /dev/null @@ -1,18 +0,0 @@ -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.spin.input b/ticketlock-testwait/refcount.spin.input deleted file mode 100644 index d2a22d2..0000000 --- a/ticketlock-testwait/refcount.spin.input +++ /dev/null @@ -1,114 +0,0 @@ -#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 deleted file mode 100644 index 77fcc77..0000000 --- a/ticketlock-testwait/refcount_4_bits_per_byte.log +++ /dev/null @@ -1,22 +0,0 @@ -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'