LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model

被引：4

作者：

Barnat, Jiri ^{[1
]}

Brim, Lubos ^{[1
]}

Havel, Vojtech ^{[1
]}

机构：

[1] Masaryk Univ, Fac Informat, Brno, Czech Republic

来源：

2013 13TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD 2013) | 2013年

关键词：

D O I：

10.1109/ACSD.2013.8

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Model checking of parallel programs under relaxed memory models has been so far limited to the verification of safety properties. Tools have been developed to automatically synthesise correct placement of synchronisation primitives to reinstate the sequential consistency. However, in practice it is not the sequential consistency that is demanded, but the correctness of the program with respect to its specification. In this paper, we introduce a new explicit-state Linear Temporal Logic model checking procedure that allows for full LTL verification of programs under approximated Total Store Order memory model. We also present a workflow of automated procedure to place the synchronisation primitives into the system under inspection to make it satisfy the given specification under the approximated memory model. Our experimental evaluation has been conducted within DiVinE - our parallel and distributed-memory LTL model checker.

引用

页码：51 / 59

页数：9

共 24 条

[1]

Abdulla PA, 2012, LECT NOTES COMPUT SC, V7214, P204, DOI 10.1007/978-3-642-28756-5_15

[2]

Alglave Jade, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P50, DOI 10.1007/978-3-642-22110-1_6

[3]

[Anonymous], PAR DISTR METH VERF

[4]

[Anonymous], 1994, The SPARC architecture manual

[5]

ATIG MF, 2010, P 37 ANN ACM SIGPLAN, V45, P7

[6]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[7]

Barnat J., 2012, NASA Formal Methods. Proceedings of the 4th International Symposium, NFM 2012, P252, DOI 10.1007/978-3-642-28891-3_25

[8]

Barnat Jiri, 2010, Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010), P222, DOI 10.1109/SEFM.2010.35

[9]

Burckhardt S, 2008, LECT NOTES COMPUT SC, V5123, P107

[10]

BURNIM J, 2010, UCBEECS201031

← 1 2 3 →