-
Notifications
You must be signed in to change notification settings - Fork 0
/
thesis.bib
3850 lines (3592 loc) · 208 KB
/
thesis.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
@book{norris,
place={Cambridge},
series={Cambridge Series in Statistical and Probabilistic Mathematics},
title={Markov Chains},
DOI={10.1017/CBO9780511810633},
publisher={Cambridge University Press},
author={Norris, James R.},
year={1997},
collection={Cambridge Series in Statistical and Probabilistic Mathematics}
}
@book{Baier2008,
author = {Baier, Christel and Katoen, Joost-Pieter},
title = {Principles of Model Checking},
year = {2008},
isbn = {978-0-262-02649-9},
publisher = {The MIT Press},
}
@InProceedings{SVC19,
author = {Dirk Beyer},
title = {Automatic Verification of {C} and Java Programs: {SV-COMP} 2019},
booktitle = {Proc.\ TACAS, part 3},
series = {LNCS~11429},
publisher = {Springer},
pages = {133-155},
year = {2019},
doi = {10.1007/978-3-030-17502-3\_9},
pdf = {https://doi.org/10.1007/978-3-030-17502-3\_9},
url = {https://sv-comp.sosy-lab.org/2019/}
}
@ARTICLE{CC14,
author={Yan {Cai} and W. K. {Chan}},
journal={IEEE Transactions on Software Engineering},
title={Magiclock: Scalable Detection of Potential Deadlocks in Large-Scale Multithreaded Programs},
year={2014},
volume={40},
number={3},
pages={266-281},
keywords={concurrency control;multi-threading;operating systems (computers);system recovery;Magiclock;potential deadlocks scalable detection;large-scale multithreaded programs;potential deadlock localization;lock order graph;scalability;System recovery;Message systems;Classification algorithms;Instruction sets;Image edge detection;Monitoring;Multicore processing;Deadlock detection;multithreaded programs;concurrency;lock order graph;scalability},
doi={10.1109/TSE.2014.2301725},
ISSN={0098-5589},
month={3}
}
@article{agarwal2010detection,
title={Detection of Deadlock Potentials in Multithreaded Programs},
author={Agarwal, Rahul and Bensalem, Saddek and Farchi, Eitan and Havelund, Klaus and Nir-Buchbinder, Yarden and Stoller, Scott D and Ur, Shmuel and Wang, Liqiang},
journal={IBM Journal of Research and Development},
volume={54},
number={5},
pages={3--1},
year={2010},
publisher={IBM},
doi="10.1147/JRD.2010.2060276"
}
@article{bensalem2005scalable,
title={Scalable dynamic deadlock analysis of multi-threaded programs},
author={Bensalem, Saddek and Havelund, Klaus},
journal={Parallel and Distributed Systems: Testing and Debugging},
volume={2005},
year={2005},
url={https://www.researchgate.net/profile/Klaus_Havelund/publication/221471856_Dynamic_Deadlock_Analysis_of_Multi-threaded_Programs/links/02bfe51368e93ccaa4000000.pdf}
}
@Article{Chaki2005,
author="Chaki, Sagar
and Clarke, Edmund
and Ouaknine, Jo{\"e}l
and Sharygina, Natasha
and Sinha, Nishant",
title="Concurrent software verification with states, events, and deadlocks",
journal="Formal Aspects of Computing",
year="2005",
month={12},
day="01",
volume="17",
number="4",
pages="461--483",
abstract="We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification.",
issn="1433-299X",
doi="10.1007/s00165-005-0071-z",
_url="https://doi.org/10.1007/s00165-005-0071-z"
}
@article{Demartini99,
author = {Demartini, Claudio and Iosif, Radu and Sisto, Riccardo},
title = {A deadlock detection tool for concurrent Java programs},
journal = {Software: Practice and Experience},
volume = {29},
number = {7},
pages = {577-603},
keywords = {concurrent programming, deadlock, formal analysis, Java, PROMELA, SPIN},
doi = {10.1002/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V},
_url = {https://onlinelibrary.wiley.com/doi/abs/10.1002/%28SICI%291097-024X%28199906%2929%3A7%3C577%3A%3AAID-SPE246%3E3.0.CO%3B2-V},
_eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1002/%28SICI%291097-024X%28199906%2929%3A7%3C577%3A%3AAID-SPE246%3E3.0.CO%3B2-V},
year = {1999}
}
@inproceedings{Ng2016,
author = {Ng, Nicholas and Yoshida, Nobuko},
title = {{Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis}},
booktitle = {Proceedings of the 25th International Conference on Compiler Construction},
series = {CC 2016},
year = {2016},
isbn = {978-1-4503-4241-4},
location = {Barcelona, Spain},
pages = {174--184},
numpages = {11},
_url = {http://doi.acm.org/10.1145/2892208.2892232},
doi = {10.1145/2892208.2892232},
acmid = {2892232},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Communication safety, Concurrent Go, Deadlock freedom, Session types, Static Analysis, Synthesis, Type safety},
}
@Article{Giesl2017,
author="Giesl, J{\"u}rgen and Aschermann, Cornelius and Brockschmidt, Marc
and Emmes, Fabian and Frohn, Florian and Fuhs, Carsten and Hensel, Jera
and Otto, Carsten and Pl{\"u}cker, Martin and Schneider-Kamp, Peter and
Str{\"o}der, Thomas and Swiderski, Stephanie and Thiemann, Ren{\'e}",
title="Analyzing Program Termination and Complexity Automatically with AProVE",
journal="Journal of Automated Reasoning",
year="2017",
month="1",
day="01",
volume="58",
number="1",
pages="3--31",
abstract="In this system description, we present the tool AProVE for automatic termination and complexity proofs of Java, C, Haskell, Prolog, and rewrite systems. In addition to classical term rewrite systems (TRSs), AProVE also supports rewrite systems containing built-in integers (int-TRSs). To analyze programs in high-level languages, AProVE automatically converts them to (int-)TRSs. Then, a wide range of techniques is employed to prove termination and to infer complexity bounds for the resulting rewrite systems. The generated proofs can be exported to check their correctness using automatic certifiers. To use AProVE in software construction, we present a corresponding plug-in for the popular Eclipse software development environment.",
issn="1573-0670",
doi="10.1007/s10817-016-9388-y",
_url="https://doi.org/10.1007/s10817-016-9388-y"
}
@inproceedings{Chen2018,
author = {Chen, Yu-Fang and Heizmann, Matthias and Leng\'{a}l, Ond\v{r}ej and Li, Yong and Tsai, Ming-Hsien and Turrini, Andrea and Zhang, Lijun},
title = {Advanced Automata-based Algorithms for Program Termination Checking},
booktitle = {Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation},
series = {PLDI 2018},
year = {2018},
isbn = {978-1-4503-5698-5},
location = {Philadelphia, PA, USA},
pages = {135--150},
numpages = {16},
_url = {http://doi.acm.org/10.1145/3192366.3192405},
doi = {10.1145/3192366.3192405},
acmid = {3192405},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {B\"{u}chi Automata Complementation and Language Difference, Program Termination},
}
@inproceedings{Alglave2013,
author="Alglave, Jade and Kroening, Daniel and Nimal, Vincent and Tautschnig, Michael",
_editor="Felleisen, Matthias and Gardner, Philippa",
title="{Software Verification for Weak Memory via Program Transformation}",
bookTitle="ESOP",
year="2013",
publisher="Springer",
address="Berlin, Heidelberg",
pages="512--532",
_isbn="978-3-642-37036-6",
doi="10.1007/978-3-642-37036-6_28",
_url="http://dx.doi.org/10.1007/978-3-642-37036-6_28",
_read=1,
_tags="memory model",
_related_raw="[3,7] write atomicity relaxation, 6 RMO, 2 TSO sound and complete procedure, [4,5] axiomatic model and stability",
_related="Alglave2010_fences memory model description",
_summary="Transformation for adding memory models (parametrized from TSO to POWER) to goto-programs together with optimization of the number of delays."
}
@InProceedings{Alglave2013po,
author="Alglave, Jade
and Kroening, Daniel
and Tautschnig, Michael",
editor="Sharygina, Natasha
and Veith, Helmut",
title="Partial Orders for Efficient Bounded Model Checking of Concurrent Software",
booktitle="Computer Aided Verification",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="141--157",
abstract="The number of interleavings of a concurrent program makes automatic analysis of such software very hard. Modern multiprocessors' execution models make this problem even harder. Modelling program executions with partial orders rather than interleavings addresses both issues: we obtain an efficient encoding into integer difference logic for bounded model checking that enables first-time formal verification of deployed concurrent systems code. We implemented the encoding in the CBMC tool and present experiments over a wide range of memory models, including SC, Intel x86 and IBM Power. Our experiments include core parts of PostgreSQL, the Linux kernel and the Apache HTTP server.",
isbn="978-3-642-39799-8",
doi="10.1007/978-3-642-39799-8_9"
}
@Inbook{Alglave2010_fences,
author="Alglave, Jade and Maranget, Luc and Sarkar, Susmit and Sewell, Peter",
editor="Touili, Tayssir and Cook, Byron and Jackson, Paul",
title="Fences in Weak Memory Models",
bookTitle="Computer Aided Verification",
year="2010",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="258--272",
_isbn="978-3-642-14295-6",
doi="10.1007/978-3-642-14295-6_25",
_url="http://dx.doi.org/10.1007/978-3-642-14295-6_25",
_read=1,
_tags="memory model",
_related_raw="[3] shared memory intro, [4] POWER, [10], [11] verifying memory coherence, [19] Java memory model + thin air, [23], [25] operational model, [26] axiomatic model",
_summary="Axiomatic description of memory models and recovering of stronger
model from weaker using fences."
}
@inproceedings{wmdecidability,
author = {Atig, Mohamed Faouzi and Bouajjani, Ahmed and Burckhardt, Sebastian and Musuvathi, Madanlal},
title = {{On the Verification Problem for Weak Memory Models}},
booktitle = {POPL},
year = {2010},
_isbn = {978-1-60558-479-9},
location = {Madrid, Spain},
pages = {7--18},
numpages = {12},
_url = {http://doi.acm.org/10.1145/1706299.1706303},
doi = {10.1145/1706299.1706303},
acmid = {1706303},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {infinite state systems, lossy channel systems, program verification, relaxed memory models},
_tags="memory model",
_read=1,
_summary="Complexity and decidability analisys for memory models, showing
TSO/PSO is non-elementary and RMO is undecidable, rather theoretical"
}
@inproceedings{Bouajjani2015,
author="Bouajjani, Ahmed and Calin, Georgel and Derevenetc, Egor and Meyer, Roland",
_editor="Egyed, Alexander and Schaefer, Ina",
title="{Lazy TSO Reachability}",
bookTitle="FASE",
year="2015",
publisher="Springer",
address="Berlin, Heidelberg",
pages="267--282",
_isbn="978-3-662-46675-9",
doi="10.1007/978-3-662-46675-9_18",
_url="http://dx.doi.org/10.1007/978-3-662-46675-9_18",
_related = "wmdecidability, Bouajjani2013 10 robustness",
_read=1,
_summary="TSO semi-decision procedure, lazyly extends runs with TSO
semantics (starting from SC), complete only for acyclic programs. Uses
robustness checker to detect which runs should be relaxed. On automata,
not on programs."
}
@InProceedings{Bouajjani2013,
author="Bouajjani, Ahmed and Derevenetc, Egor and Meyer, Roland",
_editor="Felleisen, Matthias and Gardner, Philippa",
title="{Checking and Enforcing Robustness against TSO}",
bookTitle="ESOP",
year="2013",
publisher="Springer",
address="Berlin, Heidelberg",
pages="533--553",
_isbn="978-3-642-37036-6",
doi="10.1007/978-3-642-37036-6_29",
_url="http://dx.doi.org/10.1007/978-3-642-37036-6_29",
_read=1,
_summary="A reduction from TSO robustness/stability (all TSO traces
correspond to some SC trace), to multiple SC reachability queries in
instrumented program (which has limited buffering in one thered). The
reduction requires O(n^2) queries and requires that all pairs of loads
and stores for given thread are enumerated.",
_related_raw = "[3] DRF programs",
}
@inproceedings{Burckhardt2008,
author="Burckhardt, Sebastian and Musuvathi, Madanlal",
_editor="Gupta, Aarti and Malik, Sharad",
title="Effective Program Verification for Relaxed Memory Models",
bookTitle="CAV",
year="2008",
publisher="Springer",
address="Berlin, Heidelberg",
pages="107--120",
_isbn="978-3-540-70545-1",
doi="10.1007/978-3-540-70545-1_12",
_url="http://dx.doi.org/10.1007/978-3-540-70545-1_12",
_todo="0.5",
_read="0.2",
_related_raw = "[18] SC, [24] TSO",
_summary = "detection of SC violations using a monitor with generalized
vector clock, tool Sober"
}
@inproceedings{Burnim2011,
author="Burnim, Jabob and Sen, Koushik and Stergiou, Christos",
_editor="Abdulla, Parosh Aziz and Leino, K. Rustan M.",
title="{Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models}",
bookTitle="TACAS",
year="2011",
publisher="Springer",
address="Berlin, Heidelberg",
pages="11--25",
_isbn="978-3-642-19835-9",
doi="10.1007/978-3-642-19835-9_3",
_url="http://dx.doi.org/10.1007/978-3-642-19835-9_3",
_read="0.2",
_todo=1,
_summary="monitors for detecting violations of SC under TSO or PSO, using
operational semantics of TSO/PSO"
}
@inproceedings{Alglave2011,
author="Alglave, Jade and Maranget, Luc",
_editor="Gopalakrishnan, Ganesh and Qadeer, Shaz",
title="{Stability in Weak Memory Models}",
bookTitle="CAV",
year="2011",
publisher="Springer",
address="Berlin, Heidelberg",
pages="50--66",
_isbn="978-3-642-22110-1",
doi="10.1007/978-3-642-22110-1_6",
_url="http://dx.doi.org/10.1007/978-3-642-22110-1_6",
_related_raw="[3] DRF guarantee",
_summary = "notion of stability of executions from one memory model to a
weaker one, tool offence for inserting synchronization to x86 and POWER
assembly to ensure stability",
_read=1,
}
@ARTICLE{Holzmann1997,
author={Gerard J. Holzmann},
journal={IEEE Transactions on Software Engineering},
title={{The model checker SPIN}},
year={1997},
volume={23},
number={5},
pages={279-295},
keywords={distributed processing;formal specification;formal
verification;SPIN model checker;design error detection;detailed
code;distributed software system models;efficient verification
system;high-level distributed algorithm descriptions;telephone
exchange control;verifier design;verifier structure;Algorithm design
and analysis;Application software;Concurrent computing;Control
system synthesis;Design methodology;Distributed algorithms;Error
correction codes;Message passing;Software systems;Telephony},
doi={10.1109/32.588521},
ISSN={0098-5589},
month=5,
}
@inproceedings{cppmemmod,
author = {Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark},
title = {Mathematizing C++ Concurrency},
booktitle = {Principles of Programming Languages},
series = {POPL '11},
year = {2011},
_isbn = {978-1-4503-0490-0},
location = {Austin, Texas, USA},
pages = {55--66},
numpages = {12},
_url = {http://doi.acm.org/10.1145/1926385.1926394},
doi = {10.1145/1926385.1926394},
acmid = {1926394},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {relaxed memory models, semantics},
_read=1,
_summary="Axiomatic description of C++ memory model, with some divergencies from the standard draft N3092 (final is ??).",
}
@article{x86tso,
author = {Sewell, Peter and Sarkar, Susmit and Owens, Scott and Nardelli, Francesco Zappa and Myreen, Magnus O.},
title = {{X86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors}},
journal = {Communications of the ACM},
issue_date = {July 2010},
volume = {53},
number = {7},
month = jul,
year = {2010},
issn = {0001-0782},
pages = {89--97},
numpages = {9},
_url = {http://doi.acm.org/10.1145/1785414.1785443},
doi = {10.1145/1785414.1785443},
acmid = {1785443},
publisher = {ACM},
address = {New York, NY, USA},
_read=1,
_summary="Description of the x86 memory model, formalized in HOL4 and as an
abstract machine. Also discusses problems with informal specification.",
_related_raw="[9] Causal memory, [33] program transformations in java vs. memory model"
}
@article{hw_view_for_sw_hackers,
title={Memory barriers: a hardware view for software hackers},
author={Paul E McKenney},
journal={Linux Technology Center, IBM Beaverton},
year={2010},
}
@inproceedings{PichonPharabod2016,
author = {Pichon-Pharabod, Jean and Sewell, Peter},
title = {A Concurrency Semantics for Relaxed Atomics That Permits Optimisation and Avoids Thin-air Executions},
booktitle = {Principles of Programming Languages},
series = {POPL '16},
year = {2016},
_isbn = {978-1-4503-3549-2},
location = {St. Petersburg, FL, USA},
pages = {622--633},
numpages = {12},
_url = {http://doi.acm.org/10.1145/2837614.2837616},
doi = {10.1145/2837614.2837616},
acmid = {2837616},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {C/C++, Concurrency, Relaxed memory models},
_read = 1,
_summary = "An alternative way of defining semantics for non-atomic and
relaxed atomic operations, aiming to both avoid thin air reads and
enable optimization. Targets C++. The semantics is based on event
structures and analyze all runs at the same time, considering possible
optimizations.",
_related = "event_structures, Sevcik2008 java memory model problems"
}
@Inbook{event_structures,
author="Nielsen, Mogens and Plotkin, Gordon and Winskel, Glynn",
editor="Kahn, Gilles",
title="Petri nets, event structures and domains",
bookTitle="Semantics of Concurrent Computation",
year="1979",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="266--284",
_isbn="978-3-540-35163-4",
doi="10.1007/BFb0022474",
_url="http://dx.doi.org/10.1007/BFb0022474",
_read = 0
}
@Inbook{Sevcik2008,
author="{\v{S}}ev{\v{c}}{\'i}k, Jaroslav and Aspinall, David",
editor="Vitek, Jan",
title="On Validity of Program Transformations in the Java Memory Model",
bookTitle="European Conference on Object-Oriented Programming",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="27--51",
_isbn="978-3-540-70592-5",
doi="10.1007/978-3-540-70592-5_3",
_url="http://dx.doi.org/10.1007/978-3-540-70592-5_3",
_read="0.2",
_related_raw = "[11][18] Java Memory Model, [20] JMM is fatally flawed,
[16][1][9][23] SC guarantees for DRF programs"
}
@book{javamm_Gosling2005,
author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad},
title = {The Java(TM) Language Specification (3rd Edition)},
year = {2005},
_isbn = {0321246780},
publisher = {Addison-Wesley Professional},
}
@inproceedings{javamm_popl_Manson2005,
author = {Manson, Jeremy and Pugh, William and Adve, Sarita V.},
title = {The Java Memory Model},
booktitle = {Principles of Programming Languages},
series = {POPL '05},
year = {2005},
_isbn = {1-58113-830-X},
location = {Long Beach, California, USA},
pages = {378--391},
numpages = {14},
_url = {http://doi.acm.org/10.1145/1040305.1040336},
doi = {10.1145/1040305.1040336},
acmid = {1040336},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Java, concurrency, memory model, multithreading},
}
@article{post1946variant,
title={A variant of a recursively unsolvable problem},
author={Post, Emil L},
journal={Bulletin of the American Mathematical Society},
volume={52},
number={4},
pages={264--268},
year={1946}
}
@article{abdulla1996verifying,
title={Verifying programs with unreliable channels},
author={Abdulla, Parosh Aziz and Jonsson, Bengt},
journal={Information and Computation},
volume={127},
number={2},
pages={91--101},
year={1996},
publisher={Elsevier}
}
@article{abdulla1996undecidable,
title={Undecidable verification problems for programs with unreliable
channels},
author={Abdulla, Parosh Aziz and Jonsson, Bengt},
journal={Information and Computation},
volume={130},
number={1},
pages={71--90},
year={1996},
publisher={Elsevier},
_read="0.1",
_summary = "can be combined with [wmdecidability] to prove that LTL and CTL
model checking is undecidable for TSO"
}
@Inbook{Atig2012,
author="Atig, Mohamed Faouzi and Bouajjani, Ahmed and Burckhardt, Sebastian and Musuvathi, Madanlal",
editor="Seidl, Helmut",
title="What's Decidable about Weak Memory Models?",
bookTitle="European Symposium on Programming",
year="2012",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="26--46",
_isbn="978-3-642-28869-2",
doi="10.1007/978-3-642-28869-2_2",
_url="http://dx.doi.org/10.1007/978-3-642-28869-2_2"
}
@Inbook{Abdulla2012,
author="Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Chen, Yu-Fang and Leonardsson, Carl and Rezine, Ahmed",
editor="Flanagan, Cormac and K{\"o}nig, Barbara",
title="Counter-Example Guided Fence Insertion under TSO",
bookTitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2012",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="204--219",
_isbn="978-3-642-28756-5",
doi="10.1007/978-3-642-28756-5_15",
_url="http://dx.doi.org/10.1007/978-3-642-28756-5_15"
}
@inproceedings{Linden2010,
author="Linden, Alexander and Wolper, Pierre",
_editor="van de Pol, Jaco and Weber, Michael",
title="{An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models}",
bookTitle="SPIN",
year="2010",
publisher="Springer",
address="Berlin, Heidelberg",
pages="212--226",
_isbn="978-3-642-16164-3",
doi="10.1007/978-3-642-16164-3_16",
_url="http://dx.doi.org/10.1007/978-3-642-16164-3_16"
}
@inproceedings{Atig2011,
author="Atig, Mohamed Faouzi and Bouajjani, Ahmed and Parlato, Gennaro",
_editor="Gopalakrishnan, Ganesh and Qadeer, Shaz",
title="Getting Rid of Store-Buffers in TSO Analysis",
bookTitle="CAV",
year="2011",
publisher="Springer",
address="Berlin, Heidelberg",
pages="99--115",
_isbn="978-3-642-22110-1",
doi="10.1007/978-3-642-22110-1_9",
_url="http://dx.doi.org/10.1007/978-3-642-22110-1_9"
}
@inproceedings{Park1995,
author = {Park, Seungjoon and Dill, David L.},
title = {{An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order)}},
booktitle = {SPAA},
year = {1995},
_isbn = {0-89791-717-0},
location = {Santa Barbara, California, USA},
pages = {34--41},
numpages = {8},
_url = {http://doi.acm.org/10.1145/215399.215413},
doi = {10.1145/215399.215413},
acmid = {215413},
publisher = {ACM},
address = {New York, NY, USA},
_read = 1,
_summary = "SPARC, encoding to murphi, simple synchronization primitives
only, explores all allowed reordering of instructions"
}
@inproceedings{Abdulla2017,
author="Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Bouajjani, Ahmed and Ngo, Tuan Phong",
_editor="Legay, Axel and Margaria, Tiziana",
title="Context-Bounded Analysis for POWER",
bookTitle="TACAS",
year="2017",
publisher="Springer",
address="Berlin, Heidelberg",
pages="56--74",
_isbn="978-3-662-54580-5",
doi="10.1007/978-3-662-54580-5_4",
_url="https://doi.org/10.1007/978-3-662-54580-5_4",
_read="0.5",
_summary = "Context bounded analysis for the POWER architecture, by
transformation of program. CBMC is used as a backend. It shows that context
bounded analysis for POWER is decidable. Tool `power2sc`, compared with
goto-instrument and niddhug. Evaluation on C programs."
}
@article{Abdulla2017tso,
title={Stateless model checking for TSO and PSO},
author={Abdulla, Parosh Aziz and Aronis, Stavros and Atig, Mohamed Faouzi and Jonsson, Bengt and Leonardsson, Carl and Sagonas, Konstantinos},
journal={Acta Informatica},
volume={54},
number={8},
pages={789--818},
year={2017},
publisher={Springer},
doi={10.1007/s00236-016-0275-0}
}
@inproceedings{Turon2014,
author = {Turon, Aaron and Vafeiadis, Viktor and Dreyer, Derek},
title = {{GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation}},
booktitle = {OOPSLA},
year = {2014},
_isbn = {978-1-4503-2585-1},
location = {Portland, Oregon, USA},
pages = {691--707},
numpages = {17},
_url = {http://doi.acm.org/10.1145/2660193.2660243},
doi = {10.1145/2660193.2660243},
acmid = {2660243},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {c/c++, concurrency, program logic, separation logic, weak memory models},
_read = "0.3",
_summary = "Introduces a separation logic GPS which allows proving properties
about programs using the (fragment of) C11 memory model. The memory models
is restricted to non-atomic, acquire-release, and sequentially consistent
accesses -- i.e. it lacks support for relaxed and consume-release accesses."
}
@inproceedings{Dan2013,
author="Dan, Andrei Marian and Meshman, Yuri and Vechev, Martin and Yahav, Eran",
_editor="Logozzo, Francesco and F{\"a}hndrich, Manuel",
title="{Predicate Abstraction for Relaxed Memory Models}",
bookTitle="SAS",
year="2013",
publisher="Springer",
address="Berlin, Heidelberg",
pages="84--104",
abstract="We present a novel approach for predicate abstraction of programs
running on relaxed memory models. Our approach consists of two steps.",
_isbn="978-3-642-38856-9",
doi="10.1007/978-3-642-38856-9_7",
_url="https://doi.org/10.1007/978-3-642-38856-9_7",
_read = "0.5",
_summary = "Presents an approach for verification of (potentially
infinite state space) programs under TSO and PSO using predicate
abstraction. The paper first shows that it is not possible to use
traditional predicate abstraction to produce boolean program and then
verify this boolean program using weak memory semantics. Instead, the
authors propose a schema which first verifies the program under SC and
then extrapolates predicates from SC run to verify a transformed version of
the original program which has store buffers explicitly encoded. The
store buffers are bounded in this transformation. Authors also provide
implementation in the \textsc{cupex} and evaluation on 7 programs which
shows advantages of their predicate extrapolation method."
}
@inproceedings{Yang2004,
author="Yang, Yue and Gopalakrishnan, Ganesh and Lindstrom, Gary",
_editor="Davies, Jim and Schulte, Wolfram and Barnett, Mike",
title="{Memory-Model-Sensitive Data Race Analysis}",
bookTitle="ICFEM",
year="2004",
publisher="Springer",
address="Berlin, Heidelberg",
pages="30--45",
abstract="We present a ``memory-model-sensitive'' approach to validating
correctness properties for multithreaded programs. Our key insight is
that by specifying both the inter-thread memory consistency model and
the intra-thread program semantics as constraints, a program
verification task can be reduced to an equivalent constraint solving
problem, thus allowing an exhaustive examination of all thread
interleavings precisely allowed by a given memory model. To demonstrate,
this paper formalizes race conditions according to the new Java memory
model, for a simplified but non-trivial source language. We then
describe the implementation of a memory-model-sensitive race detector
using constraint logic programming (CLP). In comparison with
conventional program analysis, our approach does not offer the same kind
of performance and scalability due to the complexity involved in exact
formal reasoning. However, we show that a formal semantics can serve
more than documentation purposes --- it can be applied as a sound basis
for rigorous property checking, upon which more scalable methods can be
derived.",
_isbn="978-3-540-30482-1",
doi="10.1007/978-3-540-30482-1_11",
_url="https://doi.org/10.1007/978-3-540-30482-1_11",
_read=1,
_summary = "Presents formal semantics for a simple programming language
including its precise memory semantics.
The motivation is to provide verification procedure for detecting data
races under the Java Memory Model (JMM).
The formalization uses SC as it is sufficient for detection of data
races under JMM (JMM defines data race freedom in terms on SC runs).
The entire program, memory constraits, and specification is encoded as
constraint solving problem, which can be solved by constraint solver,
e.g. Prolog with finite domain data as used in the presented tool
*DefectFindrer*."
}
@inproceedings{Huynh2006,
author="Huynh, Thuan Quang and Roychoudhury, Abhik",
_editor="Misra, Jayadev and Nipkow, Tobias and Sekerinski, Emil",
title="{A Memory Model Sensitive Checker for C{\#}}",
bookTitle="FM",
year="2006",
publisher="Springer",
address="Berlin, Heidelberg",
pages="476--491",
abstract="Modern concurrent programming languages like Java and C{\#} have a
programming language level memory model; it captures the set of all
allowed behaviors of programs on any implementation platform --- uni- or
multi-processor. Such a memory model is typically weaker than Sequential
Consistency and allows reordering of operations within a program thread.
Therefore, programs verified correct by assuming Sequential Consistency
(that is, each thread proceeds in program order) may not behave
correctly on certain platforms! The solution to this problem is to
develop program checkers which are memory model sensitive. In this
paper, we develop such an invariant checker for the programming language
C{\#}. Our checker identifies program states which are reached only
because the C{\#} memory model is more relaxed than Sequential
Consistency. Furthermore, our checker identifies (a) operation
reorderings which cause such undesirable states to be reached, and (b)
simple program modifications --- by inserting memory barrier operations
--- which prevent such undesirable reorderings.",
_isbn="978-3-540-37216-5",
doi="10.1007/11813040_32",
_url="https://doi.org/10.1007/11813040_32",
_summary="Presents explicit state model checker for C# programs (supporting
subset of C#/.NET bytecode) which uses the .NET memory model. The
verifier first verifies program under SC and then it explores additional
runs allowed under .NET memory model. It can also insert barriers into
the program to avoid relaxed runs which violate given property (that is,
not all relaxed runs are disabled by barriers but only those
that actually lead to property violation). The implementation
of the exploration algorithm uses list of delayed instructions to
implement instruction reordering. While the authors mention that the
number of reordered instructions is not bounded, they do not discuss how
this approach works for programs with cycles.",
_read=1
}
@article{Arvind2006,
author = {Arvind, Arvind and Maessen, Jan-Willem},
title = {Memory Model = Instruction Reordering + Store Atomicity},
journal = {ACM SIGARCH Computer Architecture News},
issue_date = {May 2006},
volume = {34},
number = {2},
month = may,
year = {2006},
issn = {0163-5964},
pages = {29--40},
numpages = {12},
_url = {http://doi.acm.org/10.1145/1150019.1136489},
doi = {10.1145/1150019.1136489},
acmid = {1136489},
publisher = {ACM},
address = {New York, NY, USA},
_read = 1,
}
@book{SPARC94,
author = {SPARC International, Inc.},
title = {The SPARC Architecture Manual},
editor = {David L. Weaver and Tom Germond},
subtitle = {Version 9},
year = {1994},
isbn = {0-13-825001-4},
publisher = {PTR Prentice Hall},
address = {Englewood Cliffs, New Jersey, USA},
url={http://sparc.org/wp-content/uploads/2014/01/SPARCV9.pdf.gz}
}
@inproceedings{Zhang2015,
author = {Zhang, Naling and Kusano, Markus and Wang, Chao},
title = {{Dynamic Partial Order Reduction for Relaxed Memory Models}},
booktitle = {PLDI},
year = {2015},
_isbn = {978-1-4503-3468-6},
location = {Portland, OR, USA},
pages = {250--259},
numpages = {10},
_url = {http://doi.acm.org/10.1145/2737924.2737956},
doi = {10.1145/2737924.2737956},
acmid = {2737956},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {DPOR, PSO, Stateless model checking, TSO, partial order reduction, relaxed memory model, runtime verification},
}
@inproceedings{Norris2013,
author = {Norris, Brian and Demsky, Brian},
title = {{CDSchecker: Checking Concurrent Data Structures Written with C/C++ Atomics}},
booktitle = {OOPSLA},
year = {2013},
_isbn = {978-1-4503-2374-1},
location = {Indianapolis, Indiana, USA},
pages = {131--150},
numpages = {20},
_url = {http://doi.acm.org/10.1145/2509136.2509514},
doi = {10.1145/2509136.2509514},
acmid = {2509514},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {model checking, relaxed memory model},
}
@inproceedings{Sarkar2011,
author = {Sarkar, Susmit and Sewell, Peter and Alglave, Jade and Maranget,
Luc and Williams, Derek},
title = {{Understanding POWER Multiprocessors}},
booktitle = {PLDI},
year = {2011},
_isbn = {978-1-4503-0663-8},
location = {San Jose, California, USA},
pages = {175--186},
numpages = {12},
_url = {http://doi.acm.org/10.1145/1993498.1993520},
doi = {10.1145/1993498.1993520},
acmid = {1993520},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {relaxed memory models, semantics},
}
@inproceedings{Derevenetc2014,
author="Derevenetc, Egor and Meyer, Roland",
_editor="Esparza, Javier and Fraigniaud, Pierre and Husfeldt, Thore and Koutsoupias, Elias",
title="{Robustness against Power is PSpace-complete}",
bookTitle="ICAPL",
year="2014",
publisher="Springer",
address="Berlin, Heidelberg",
pages="158--170",
abstract="Power is a RISC architecture developed by IBM, Freescale, and several other companies and implemented in a series of POWER processors. The architecture features a relaxed memory model providing very weak guarantees with respect to the ordering and atomicity of memory accesses.",
_isbn="978-3-662-43951-7",
doi="10.1007/978-3-662-43951-7_14",
_url="https://doi.org/10.1007/978-3-662-43951-7_14"
}
@Inbook{Aspinall2007,
author="Aspinall, David and {\v{S}}ev{\v{c}}{\'i}k, Jaroslav",
editor="Schneider, Klaus and Brandt, Jens",
title="Formalising Java's Data Race Free Guarantee",
bookTitle="Theorem Proving in Higher Order Logics",
year="2007",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="22--37",
_isbn="978-3-540-74591-4",
doi="10.1007/978-3-540-74591-4_4",
_url="https://doi.org/10.1007/978-3-540-74591-4_4"
}
@InProceedings{MadorHaim2012,
author="Mador-Haim, Sela and Maranget, Luc and Sarkar, Susmit and Memarian, Kayvan and Alglave, Jade and Owens, Scott and Alur, Rajeev and Martin, Milo M. K. and Sewell, Peter and Williams, Derek",
_editor="Madhusudan, P. and Seshia, Sanjit A.",
title="{An Axiomatic Memory Model for POWER Multiprocessors}",
bookTitle="CAV",
year="2012",
publisher="Springer",
address="Berlin, Heidelberg",
pages="495--512",
_isbn="978-3-642-31424-7",
doi="10.1007/978-3-642-31424-7_36",
_url="https://doi.org/10.1007/978-3-642-31424-7_36"
}
@inproceedings{Sarkar2012,
author = {Sarkar, Susmit and Memarian, Kayvan and Owens, Scott and Batty, Mark and Sewell, Peter and Maranget, Luc and Alglave, Jade and Williams, Derek},
title = {Synchronising C/C++ and POWER},
booktitle = {Programming Language Design and Implementation},
series = {PLDI '12},
year = {2012},
_isbn = {978-1-4503-1205-9},
location = {Beijing, China},
pages = {311--322},
numpages = {12},
_url = {http://doi.acm.org/10.1145/2254064.2254102},
doi = {10.1145/2254064.2254102},
acmid = {2254102},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {relaxed memory models, semantics},
}
@inproceedings{Flur2016,
author = {Flur, Shaked and Gray, Kathryn E. and Pulte, Christopher and Sarkar, Susmit and Sezgin, Ali and Maranget, Luc and Deacon, Will and Sewell, Peter},
title = {{Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA}},
booktitle = {POPL},
year = {2016},
_isbn = {978-1-4503-3549-2},
location = {St. Petersburg, FL, USA},
pages = {608--621},
numpages = {14},
_url = {http://doi.acm.org/10.1145/2837614.2837615},
doi = {10.1145/2837614.2837615},
acmid = {2837615},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {ISA, Relaxed Memory Models, semantics},
}
@article{Alglave2014,
author = {Alglave, Jade and Maranget, Luc and Tautschnig, Michael},
title = {{Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory}},
journal = {ACM Transactions on Programming Languages and Systems},
issue_date = {July 2014},
volume = {36},
number = {2},
month = jul,
year = {2014},
issn = {0164-0925},
pages = {7:1--7:74},
articleno = {7},
numpages = {74},
_url = {http://doi.acm.org/10.1145/2627752},
doi = {10.1145/2627752},
acmid = {2627752},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Concurrency, software verification, weak memory models},
}
@article{Lamport1979,
author = {Lamport, Leslie},
title = {{How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs}},
journal = {IEEE Transactions on Computers},
issue_date = {September 1979},
volume = {28},
number = {9},
month = sep,
year = {1979},
issn = {0018-9340},
pages = {690--691},
numpages = {2},
_url = {http://dx.doi.org/10.1109/TC.1979.1675439},
doi = {10.1109/TC.1979.1675439},
acmid = {1311750},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
keywords = {Computer design, concurrent computing, hardware correctness, multiprocessing, parallel processing, parallel processing, Computer design, concurrent computing, hardware correctness, multiprocessing},
}
@Inbook{Cenciarelli2007,
author="Cenciarelli, Pietro and Knapp, Alexander and Sibilio, Eleonora",
editor="De Nicola, Rocco",
title="The Java Memory Model: Operationally, Denotationally, Axiomatically",
bookTitle="European Symposium on Programming",
year="2007",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="331--346",
abstract="A semantics to a small fragment of Java capturing the new memory model (JMM) described in the Language Specification is given by combining operational, denotational and axiomatic techniques in a novel semantic framework. The operational steps (specified in the form of SOS) construct denotational models (configuration structures) and are constrained by the axioms of a configuration theory. The semantics is proven correct with respect to the Language Specification and shown to capture many common examples in the JMM literature.",
_isbn="978-3-540-71316-6",
doi="10.1007/978-3-540-71316-6_23",
_url="https://doi.org/10.1007/978-3-540-71316-6_23"
}
@inproceedings{Torlak2010,
author = {Torlak, Emina and Vaziri, Mandana and Dolby, Julian},
title = {MemSAT: Checking Axiomatic Specifications of Memory Models},
booktitle = {Programming Language Design and Implementation},
series = {PLDI '10},
year = {2010},
_isbn = {978-1-4503-0019-3},
location = {Toronto, Ontario, Canada},
pages = {341--350},
numpages = {10},
_url = {http://doi.acm.org/10.1145/1806596.1806635},
doi = {10.1145/1806596.1806635},
acmid = {1806635},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {axiomatic specifications, bounded model checking, memory models, sat},
}
@inproceedings{Vafeiadis2013,