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