We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
LLVMVF: A Generic Approach for Verification of Multicore Software.
- Authors
Sousa, Marcelo; Sen, Alper
- Abstract
Proliferation of multicore hardware boosted the need for verification of multicore software that is running on these hardware. Multicore software demands new verification techniques different from the ones used for sequential software. Many optimized compiler frameworks are arising to address the complexities of multicore software. Among these compilers, Low Level Virtual Machine (LLVM) is especially gaining popularity because i) has a universal front-end that allows to read in many different input languages, ii) aggressive optimizations to improve code performance and quality, and iii) a well-defined intermediate bytecode representation, called LLVM IR, that allows a unified intermediate representation. In this work, we present a novel framework, called LLVM Verification Framework (LLVMVF), implemented in a purely functional language for verification of multicore software. To our knowledge, this is the first verification framework using the LLVM bytecode representation for multicore software. We present an SMT-based Bounded Model Checker backend of LLVMVF and perform initial experiments on multicore software using Pthreads library. Furthermore, we compare our results with an existing multicore software verification tool.
- Subjects
MULTICORE processors; SOFTWARE verification; VIRTUAL machine systems; CODING theory; THREADS (Computer programs)
- Publication
Journal of Electronic Testing, 2013, Vol 29, Issue 5, p635
- ISSN
0923-8174
- Publication type
Article
- DOI
10.1007/s10836-013-5405-9