X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu-controldataflow-intel-no-ipi%2Furcu_free_no_mb.spin.input.trail;fp=formal-model%2Furcu-controldataflow-intel-no-ipi%2Furcu_free_no_mb.spin.input.trail;h=39bdf85ef9fb5d675ecacdb420e9085c7a7bf025;hp=0000000000000000000000000000000000000000;hb=b6b17880a1a83b679d968907e2ff6cf72dd645fb;hpb=06e8b2a87f862183a26e0005bf04221633f49d0c

diff --git a/formal-model/urcu-controldataflow-intel-no-ipi/urcu_free_no_mb.spin.input.trail b/formal-model/urcu-controldataflow-intel-no-ipi/urcu_free_no_mb.spin.input.trail
new file mode 100644
index 0000000..39bdf85
--- /dev/null
+++ b/formal-model/urcu-controldataflow-intel-no-ipi/urcu_free_no_mb.spin.input.trail
@@ -0,0 +1,1146 @@
+-2:3:-2
+-4:-4:-4
+1:0:4000
+2:3:3920
+3:3:3923
+4:3:3923
+5:3:3926
+6:3:3934
+7:3:3934
+8:3:3937
+9:3:3943
+10:3:3947
+11:3:3947
+12:3:3950
+13:3:3960
+14:3:3968
+15:3:3968
+16:3:3971
+17:3:3977
+18:3:3981
+19:3:3981
+20:3:3984
+21:3:3990
+22:3:3994
+23:3:3995
+24:0:4000
+25:3:3997
+26:0:4000
+27:2:2761
+28:0:4000
+29:2:2767
+30:0:4000
+31:2:2768
+32:0:4000
+33:2:2770
+34:0:4000
+35:2:2771
+36:0:4000
+37:2:2772
+38:0:4000
+39:2:2773
+40:0:4000
+41:2:2774
+42:2:2775
+43:2:2779
+44:2:2780
+45:2:2788
+46:2:2789
+47:2:2793
+48:2:2794
+49:2:2802
+50:2:2807
+51:2:2811
+52:2:2812
+53:2:2820
+54:2:2821
+55:2:2825
+56:2:2826
+57:2:2820
+58:2:2821
+59:2:2825
+60:2:2826
+61:2:2834
+62:2:2839
+63:2:2846
+64:2:2847
+65:2:2854
+66:2:2859
+67:2:2866
+68:2:2867
+69:2:2866
+70:2:2867
+71:2:2874
+72:2:2884
+73:0:4000
+74:2:2773
+75:0:4000
+76:2:2888
+77:2:2892
+78:2:2893
+79:2:2897
+80:2:2901
+81:2:2902
+82:2:2906
+83:2:2914
+84:2:2915
+85:2:2919
+86:2:2923
+87:2:2924
+88:2:2919
+89:2:2920
+90:2:2928
+91:0:4000
+92:2:2773
+93:0:4000
+94:2:2936
+95:2:2937
+96:2:2938
+97:0:4000
+98:2:2773
+99:0:4000
+100:2:2946
+101:0:4000
+102:2:2773
+103:0:4000
+104:2:2949
+105:2:2950
+106:2:2954
+107:2:2955
+108:2:2963
+109:2:2964
+110:2:2968
+111:2:2969
+112:2:2977
+113:2:2982
+114:2:2983
+115:2:2995
+116:2:2996
+117:2:3000
+118:2:3001
+119:2:2995
+120:2:2996
+121:2:3000
+122:2:3001
+123:2:3009
+124:2:3014
+125:2:3021
+126:2:3022
+127:2:3029
+128:2:3034
+129:2:3041
+130:2:3042
+131:2:3041
+132:2:3042
+133:2:3049
+134:2:3058
+135:0:4000
+136:2:2773
+137:0:4000
+138:2:3062
+139:2:3063
+140:2:3064
+141:2:3076
+142:2:3077
+143:2:3081
+144:2:3082
+145:2:3090
+146:2:3095
+147:2:3099
+148:2:3100
+149:2:3108
+150:2:3109
+151:2:3113
+152:2:3114
+153:2:3108
+154:2:3109
+155:2:3113
+156:2:3114
+157:2:3122
+158:2:3127
+159:2:3134
+160:2:3135
+161:2:3142
+162:2:3147
+163:2:3154
+164:2:3155
+165:2:3154
+166:2:3155
+167:2:3162
+168:2:3175
+169:2:3176
+170:0:4000
+171:2:2773
+172:0:4000
+173:2:3183
+174:2:3184
+175:2:3188
+176:2:3189
+177:2:3197
+178:2:3198
+179:2:3202
+180:2:3203
+181:2:3211
+182:2:3216
+183:2:3220
+184:2:3221
+185:2:3229
+186:2:3230
+187:2:3234
+188:2:3235
+189:2:3229
+190:2:3230
+191:2:3234
+192:2:3235
+193:2:3243
+194:2:3248
+195:2:3255
+196:2:3256
+197:2:3263
+198:2:3268
+199:2:3275
+200:2:3276
+201:2:3275
+202:2:3276
+203:2:3283
+204:0:4000
+205:2:2773
+206:0:4000
+207:2:3294
+208:2:3295
+209:2:3299
+210:2:3300
+211:2:3308
+212:2:3309
+213:2:3313
+214:2:3314
+215:2:3322
+216:2:3327
+217:2:3331
+218:2:3332
+219:2:3340
+220:2:3341
+221:2:3345
+222:2:3346
+223:2:3340
+224:2:3341
+225:2:3345
+226:2:3346
+227:2:3354
+228:2:3359
+229:2:3366
+230:2:3367
+231:2:3374
+232:2:3379
+233:2:3386
+234:2:3387
+235:2:3386
+236:2:3387
+237:2:3394
+238:2:3403
+239:0:4000
+240:2:2773
+241:0:4000
+242:2:3407
+243:2:3408
+244:2:3409
+245:2:3421
+246:2:3422
+247:2:3426
+248:2:3427
+249:2:3435
+250:2:3440
+251:2:3444
+252:2:3445
+253:2:3453
+254:2:3454
+255:2:3458
+256:2:3459
+257:2:3453
+258:2:3454
+259:2:3458
+260:2:3459
+261:2:3467
+262:2:3472
+263:2:3479
+264:2:3480
+265:2:3487
+266:2:3492
+267:2:3499
+268:2:3500
+269:2:3499
+270:2:3500
+271:2:3507
+272:2:3519
+273:2:3520
+274:0:4000
+275:2:2773
+276:0:4000
+277:2:3529
+278:2:3530
+279:0:4000
+280:2:2773
+281:0:4000
+282:2:3534
+283:0:4000
+284:2:3542
+285:0:4000
+286:2:2768
+287:0:4000
+288:2:2770
+289:0:4000
+290:2:2771
+291:0:4000
+292:2:2772
+293:0:4000
+294:2:2773
+295:0:4000
+296:2:2774
+297:2:2775
+298:2:2779
+299:2:2780
+300:2:2788
+301:2:2789
+302:2:2793
+303:2:2794
+304:2:2802
+305:2:2807
+306:2:2811
+307:2:2812
+308:2:2820
+309:2:2821
+310:2:2822
+311:2:2820
+312:2:2821
+313:2:2825
+314:2:2826
+315:2:2834
+316:2:2839
+317:2:2846
+318:2:2847
+319:2:2854
+320:2:2859
+321:2:2866
+322:2:2867
+323:2:2866
+324:2:2867
+325:2:2874
+326:2:2884
+327:0:4000
+328:2:2773
+329:0:4000
+330:2:2888
+331:2:2892
+332:2:2893
+333:2:2897
+334:2:2901
+335:2:2902
+336:2:2906
+337:2:2914
+338:2:2915
+339:2:2919
+340:2:2920
+341:2:2919
+342:2:2923
+343:2:2924
+344:2:2928
+345:0:4000
+346:2:2773
+347:0:4000
+348:2:2936
+349:2:2937
+350:2:2938
+351:0:4000
+352:2:2773
+353:0:4000
+354:2:2946
+355:0:4000
+356:2:2773
+357:0:4000
+358:2:2949
+359:2:2950
+360:2:2954
+361:2:2955
+362:2:2963
+363:2:2964
+364:2:2968
+365:2:2969
+366:2:2977
+367:2:2982
+368:2:2983
+369:2:2995
+370:2:2996
+371:2:3000
+372:2:3001
+373:2:2995
+374:2:2996
+375:2:3000
+376:2:3001
+377:2:3009
+378:2:3014
+379:2:3021
+380:2:3022
+381:2:3029
+382:2:3034
+383:2:3041
+384:2:3042
+385:2:3041
+386:2:3042
+387:2:3049
+388:2:3058
+389:0:4000
+390:2:2773
+391:0:4000
+392:2:3062
+393:2:3063
+394:2:3064
+395:2:3076
+396:2:3077
+397:2:3081
+398:2:3082
+399:2:3090
+400:2:3095
+401:2:3099
+402:2:3100
+403:2:3108
+404:2:3109
+405:2:3113
+406:2:3114
+407:2:3108
+408:2:3109
+409:2:3113
+410:2:3114
+411:2:3122
+412:2:3127
+413:2:3134
+414:2:3135
+415:2:3142
+416:2:3147
+417:2:3154
+418:2:3155
+419:2:3154
+420:2:3155
+421:2:3162
+422:2:3175
+423:2:3176
+424:0:4000
+425:2:2773
+426:0:4000
+427:2:3183
+428:2:3184
+429:2:3188
+430:2:3189
+431:2:3197
+432:2:3198
+433:2:3202
+434:2:3203
+435:2:3211
+436:2:3216
+437:2:3220
+438:2:3221
+439:2:3229
+440:2:3230
+441:2:3234
+442:2:3235
+443:2:3229
+444:2:3230
+445:2:3234
+446:2:3235
+447:2:3243
+448:2:3248
+449:2:3255
+450:2:3256
+451:2:3263
+452:2:3268
+453:2:3275
+454:2:3276
+455:2:3275
+456:2:3276
+457:2:3283
+458:0:4000
+459:2:2773
+460:0:4000
+461:2:3294
+462:2:3295
+463:2:3299
+464:2:3300
+465:2:3308
+466:2:3309
+467:2:3313
+468:2:3314
+469:2:3322
+470:2:3327
+471:2:3331
+472:2:3332
+473:2:3340
+474:2:3341
+475:2:3345
+476:2:3346
+477:2:3340
+478:2:3341
+479:2:3345
+480:2:3346
+481:2:3354
+482:2:3359
+483:2:3366
+484:2:3367
+485:2:3374
+486:2:3379
+487:2:3386
+488:2:3387
+489:2:3386
+490:2:3387
+491:2:3394
+492:2:3403
+493:0:4000
+494:2:2773
+495:0:4000
+496:2:3407
+497:2:3408
+498:2:3409
+499:2:3421
+500:2:3422
+501:2:3426
+502:2:3427
+503:2:3435
+504:2:3440
+505:2:3444
+506:2:3445
+507:2:3453
+508:2:3454
+509:2:3458
+510:2:3459
+511:2:3453
+512:2:3454
+513:2:3458
+514:2:3459
+515:2:3467
+516:2:3472
+517:2:3479
+518:2:3480
+519:2:3487
+520:2:3492
+521:2:3499
+522:2:3500
+523:2:3499
+524:2:3500
+525:2:3507
+526:2:3519
+527:2:3520
+528:0:4000
+529:2:2773
+530:0:4000
+531:2:3529
+532:2:3530
+533:0:4000
+534:2:2773
+535:0:4000
+536:2:3534
+537:0:4000
+538:2:3542
+539:0:4000
+540:2:2768
+541:0:4000
+542:2:2770
+543:0:4000
+544:2:2771
+545:0:4000
+546:2:2772
+547:0:4000
+548:2:2773
+549:0:4000
+550:2:2774
+551:2:2775
+552:2:2779
+553:2:2780
+554:2:2788
+555:2:2789
+556:2:2793
+557:2:2794
+558:2:2802
+559:2:2807
+560:2:2811
+561:2:2812
+562:2:2820
+563:2:2821
+564:2:2825
+565:2:2826
+566:2:2820
+567:2:2821
+568:2:2822
+569:2:2834
+570:2:2839
+571:2:2846
+572:2:2847
+573:2:2854
+574:2:2859
+575:2:2866
+576:2:2867
+577:2:2866
+578:2:2867
+579:2:2874
+580:2:2884
+581:0:4000
+582:2:2773
+583:0:4000
+584:2:2888
+585:2:2892
+586:2:2893
+587:2:2897
+588:2:2901
+589:2:2902
+590:2:2906
+591:2:2914
+592:2:2915
+593:2:2919
+594:2:2923
+595:2:2924
+596:2:2919
+597:2:2920
+598:2:2928
+599:0:4000
+600:2:2773
+601:0:4000
+602:2:2936
+603:2:2937
+604:2:2938
+605:0:4000
+606:2:2773
+607:0:4000
+608:2:2946
+609:0:4000
+610:2:2773
+611:0:4000
+612:2:2949
+613:2:2950
+614:2:2954
+615:2:2955
+616:2:2963
+617:2:2964
+618:2:2968
+619:2:2969
+620:2:2977
+621:2:2990
+622:2:2991
+623:2:2995
+624:2:2996
+625:2:3000
+626:2:3001
+627:2:2995
+628:2:2996
+629:2:3000
+630:2:3001
+631:2:3009
+632:2:3014
+633:2:3021
+634:2:3022
+635:2:3029
+636:2:3036
+637:2:3037
+638:2:3041
+639:2:3042
+640:2:3041
+641:2:3042
+642:2:3049
+643:2:3058
+644:0:4000
+645:2:2773
+646:0:4000
+647:2:3062
+648:2:3063
+649:2:3064
+650:2:3076
+651:2:3077
+652:2:3081
+653:2:3082
+654:2:3090
+655:2:3103
+656:2:3104
+657:2:3108
+658:2:3109
+659:2:3113
+660:2:3114
+661:2:3108
+662:2:3109
+663:2:3113
+664:2:3114
+665:2:3122
+666:2:3127
+667:2:3134
+668:2:3135
+669:2:3142
+670:2:3149
+671:2:3150
+672:2:3154
+673:2:3155
+674:2:3154
+675:2:3155
+676:2:3162
+677:2:3175
+678:2:3176
+679:0:4000
+680:2:2773
+681:0:4000
+682:2:3183
+683:2:3184
+684:2:3188
+685:2:3189
+686:2:3197
+687:2:3198
+688:2:3202
+689:2:3203
+690:2:3211
+691:2:3224
+692:2:3225
+693:2:3229
+694:2:3230
+695:2:3234
+696:2:3235
+697:2:3229
+698:2:3230
+699:2:3234
+700:2:3235
+701:2:3243
+702:2:3248
+703:2:3255
+704:2:3256
+705:2:3263
+706:2:3270
+707:2:3271
+708:2:3275
+709:2:3276
+710:2:3275
+711:2:3276
+712:2:3283
+713:0:4000
+714:2:2773
+715:0:4000
+716:2:3407
+717:2:3408
+718:2:3412
+719:2:3413
+720:2:3421
+721:2:3422
+722:2:3426
+723:2:3427
+724:2:3435
+725:2:3448
+726:2:3449
+727:2:3453
+728:2:3454
+729:2:3458
+730:2:3459
+731:2:3453
+732:2:3454
+733:2:3458
+734:2:3459
+735:2:3467
+736:2:3472
+737:2:3479
+738:2:3480
+739:2:3487
+740:2:3494
+741:2:3495
+742:2:3499
+743:2:3500
+744:2:3499
+745:2:3500
+746:2:3507
+747:2:3519
+748:2:3520
+749:0:4000
+750:2:2773
+751:0:4000
+752:2:3529
+753:2:3530
+754:0:4000
+755:2:2773
+756:0:4000
+757:2:3294
+758:2:3295
+759:2:3299
+760:2:3300
+761:2:3308
+762:2:3309
+763:2:3313
+764:2:3314
+765:2:3322
+766:2:3335
+767:2:3336
+768:2:3340
+769:2:3341
+770:2:3342
+771:2:3340
+772:2:3341
+773:2:3345
+774:2:3346
+775:2:3354
+776:2:3359
+777:2:3366
+778:2:3367
+779:2:3374
+780:2:3381
+781:2:3382
+782:2:3386
+783:2:3387
+784:2:3386
+785:2:3387
+786:2:3394
+787:2:3403
+788:0:4000
+789:2:2773
+790:0:4000
+791:2:3534
+792:0:4000
+793:2:3542
+794:0:4000
+795:2:3543
+796:0:4000
+797:2:3548
+798:0:4000
+799:1:2
+800:0:4000
+801:2:3549
+802:0:4000
+803:1:8
+804:0:4000
+805:2:3548
+806:0:4000
+807:1:9
+808:0:4000
+809:2:3549
+810:0:4000
+811:1:10
+812:0:4000
+813:2:3548
+814:0:4000
+815:1:11
+816:0:4000
+817:2:3549
+818:0:4000
+819:1:12
+820:0:4000
+821:2:3548
+822:0:4000
+823:1:13
+824:0:4000
+825:2:3549
+826:0:4000
+827:1:14
+828:0:4000
+829:2:3548
+830:0:4000
+831:1:15
+832:0:4000
+833:2:3549
+834:0:4000
+835:1:16
+836:1:17
+837:1:21
+838:1:22
+839:1:30
+840:1:31
+841:1:35
+842:1:36
+843:1:44
+844:1:49
+845:1:53
+846:1:54
+847:1:62
+848:1:63
+849:1:67
+850:1:68
+851:1:62
+852:1:63
+853:1:67
+854:1:68
+855:1:76
+856:1:81
+857:1:88
+858:1:89
+859:1:96
+860:1:101
+861:1:108
+862:1:109
+863:1:108
+864:1:109
+865:1:116
+866:0:4000
+867:2:3548
+868:0:4000
+869:1:15
+870:0:4000
+871:2:3549
+872:0:4000
+873:1:127
+874:1:128
+875:0:4000
+876:2:3548
+877:0:4000
+878:1:15
+879:0:4000
+880:2:3549
+881:0:4000
+882:1:134
+883:1:135
+884:1:139
+885:1:140
+886:1:148
+887:1:149
+888:1:153
+889:1:154
+890:1:162
+891:1:167
+892:1:171
+893:1:172
+894:1:180
+895:1:181
+896:1:185
+897:1:186
+898:1:180
+899:1:181
+900:1:185
+901:1:186
+902:1:194
+903:1:199
+904:1:206
+905:1:207
+906:1:214
+907:1:219
+908:1:226
+909:1:227
+910:1:226
+911:1:227
+912:1:234
+913:0:4000
+914:2:3548
+915:0:4000
+916:1:15
+917:0:4000
+918:2:3549
+919:0:4000
+920:1:245
+921:1:246
+922:1:250
+923:1:251
+924:1:259
+925:1:260
+926:1:264
+927:1:265
+928:1:273
+929:1:278
+930:1:282
+931:1:283
+932:1:291
+933:1:292
+934:1:296
+935:1:297
+936:1:291
+937:1:292
+938:1:296
+939:1:297
+940:1:305
+941:1:310
+942:1:317
+943:1:318
+944:1:325
+945:1:330
+946:1:337
+947:1:338
+948:1:337
+949:1:338
+950:1:345
+951:1:354
+952:0:4000
+953:2:3548
+954:0:4000
+955:1:15
+956:0:4000
+957:2:3549
+958:0:4000
+959:1:564
+960:1:565
+961:1:569
+962:1:570
+963:1:578
+964:1:579
+965:1:580
+966:1:592
+967:1:597
+968:1:601
+969:1:602
+970:1:610
+971:1:611
+972:1:615
+973:1:616
+974:1:610
+975:1:611
+976:1:615
+977:1:616
+978:1:624
+979:1:629
+980:1:636
+981:1:637
+982:1:644
+983:1:649
+984:1:656
+985:1:657
+986:1:656
+987:1:657
+988:1:664
+989:0:4000
+990:2:3548
+991:0:4000
+992:1:15
+993:0:4000
+994:2:3549
+995:0:4000
+996:1:675
+997:1:678
+998:1:679
+999:0:4000
+1000:2:3548
+1001:0:4000
+1002:1:15
+1003:0:4000
+1004:2:3549
+1005:0:4000
+1006:1:682
+1007:1:683
+1008:1:687
+1009:1:688
+1010:1:696
+1011:1:697
+1012:1:701
+1013:1:702
+1014:1:710
+1015:1:715
+1016:1:719
+1017:1:720
+1018:1:728
+1019:1:729
+1020:1:733
+1021:1:734
+1022:1:728
+1023:1:729
+1024:1:733
+1025:1:734
+1026:1:742
+1027:1:747
+1028:1:754
+1029:1:755
+1030:1:762
+1031:1:767
+1032:1:774
+1033:1:775
+1034:1:774
+1035:1:775
+1036:1:782
+1037:0:4000
+1038:2:3548
+1039:0:4000
+1040:1:15
+1041:0:4000
+1042:2:3549
+1043:0:4000
+1044:1:906
+1045:1:907
+1046:1:911
+1047:1:912
+1048:1:920
+1049:1:921
+1050:1:925
+1051:1:926
+1052:1:934
+1053:1:939
+1054:1:943
+1055:1:944
+1056:1:952
+1057:1:953
+1058:1:957
+1059:1:958
+1060:1:952
+1061:1:953
+1062:1:957
+1063:1:958
+1064:1:966
+1065:1:971
+1066:1:978
+1067:1:979
+1068:1:986
+1069:1:991
+1070:1:998
+1071:1:999
+1072:1:998
+1073:1:999
+1074:1:1006
+1075:1:1015
+1076:1:1019
+1077:0:4000
+1078:2:3548
+1079:0:4000
+1080:1:15
+1081:0:4000
+1082:2:3549
+1083:0:4000
+1084:1:1020
+1085:1:1021
+1086:1:1025
+1087:1:1026
+1088:1:1034
+1089:1:1035
+1090:1:1036
+1091:1:1048
+1092:1:1053
+1093:1:1057
+1094:1:1058
+1095:1:1066
+1096:1:1067
+1097:1:1071
+1098:1:1072
+1099:1:1066
+1100:1:1067
+1101:1:1071
+1102:1:1072
+1103:1:1080
+1104:1:1085
+1105:1:1092
+1106:1:1093
+1107:1:1100
+1108:1:1105
+1109:1:1112
+1110:1:1113
+1111:1:1112
+1112:1:1113
+1113:1:1120
+1114:0:4000
+1115:2:3548
+1116:0:4000
+1117:1:15
+1118:0:4000
+1119:2:3549
+1120:0:4000
+1121:1:1131
+1122:0:4000
+1123:2:3548
+1124:0:4000
+1125:1:2667
+1126:1:2674
+1127:1:2675
+1128:1:2682
+1129:1:2687
+1130:1:2694
+1131:1:2695
+1132:1:2694
+1133:1:2695
+1134:1:2702
+1135:1:2706
+1136:0:4000
+1137:2:3549
+1138:0:4000
+1139:1:1133
+1140:1:1134
+1141:0:3998
+1142:2:3548
+1143:0:4004
+1144:0:4000