MODV(Memory Order Dynamic Verifier) is a fast memory consistency model verifier. Based on the conception of the time order, it implemented an effective and low time complexity algorithm for dynamically verifying relaxed memory models with synchronization blocks such as Release Consistency and Scope Consistency..
Overview
MODV is a dynamic verifier for verifying whether the execution of a concurrent test program complies with its underlying memory consistency model. There are three steps of MODV checking procedure. In step 1, a pseudo-random multi-processor test program without conditional branches is generated. In step 2, the user runs the test program on CMP system. As well as obtaining the results of the test program, the program counters are scanned periodically to obtain upper bound and lower bound of active operations. In step 3, MODV analyzer incrementally constructs the directed graph of the execution based on the result of test programs and program counters logs and checks cycles of the graph.
download
You can download the compressed executables of the latest version of MODV v0.2.2 and the manual. MODV passed the test in Linux RHEL 5.4 64bit. This version is customized for verifying the memory model of Godson-T.
publication
[1] Technical report: Efficiently and Completely Verifying Synchronized Consistency Models. Yi Lv, Luming Sun, Xiaochun Ye, Dongrui Fan, Peng Wu. ISCAS-SKLCS-14-07, 2014. PDF
[2] Efficiently and Completely Verifying Synchronized Consistency Models. Yi Lv, Luming Sun, Xiaochun Ye, Dongrui Fan, Peng Wu. In Proc. ATVA 2014, The 12th International Symposium on Automated Technology for Verification and Analysis. PDF
contact
You can contact us at our respective email addresses.