The Experts below are selected from a list of 6 Experts worldwide ranked by ideXlab platform

Stephan Falke - One of the best experts on this subject based on the ideXlab platform.

  • llbmc a bounded model checker for llvm s intermediate representation competition contribution
    Tools and Algorithms for Construction and Analysis of Systems, 2012
    Co-Authors: Carsten Sinz, Florian Merz, Stephan Falke
    Abstract:

    We present LLBMC, a bounded model checker for C programs. LLBMC uses the LLVM compiler framework in order to translate C programs into LLVM’s intermediate representation (IR). The resulting code is then converted into a logical representation and simplified using rewrite rules. The simplified formula is finally passed to an SMT solver. In contrast to many other tools, LLBMC uses a flat, bit-precise memory model. It can thus precisely model, e.g., memory-based re-interpret casts. 1 Verification Approach Bounded model checking (BMC) has proven to be a very successful technique in hardware verification. More recently, it has also been applied for verifying software written in C [1,4]. Applying BMC for verifying C programs, however, comes with many obstacles that have to be tackled. One of the most important differences is that the syntax and semantics of a programming language like C is much more complicated than a hardware description. One has to deal, e.g., with memory allocation and de-allocation, (Function) pointers, complex data structures, and Function calls. LLBMC uses an approach which, instead of exploring the source code directly, makes use of existing compiler technology and performs the analysis on a compiler intermediate representation. Such an intermediate representation offers a much simpler syntax and semantics than a programming language like C, and thus eases a logical encoding of the verification problem considerably. We have chosen the LLVM [5] compiler infrastructure and its assembler-like intermediate representation as the starting point for our approach, but the idea can also be applied to other low-level languages. LLVM is both a (GCC-compatible) C/C++/Objective-C compiler and a library of compiler technologies, providing, e.g., sourceand target-independent optimizations. Our primary goal is to detect memory errors in C code [7,2,6]. Memory errors include invalid memory accesses, heap and stack buffer overflows, and invalid frees (e.g., double frees). This work was supported in part by the “Concept for the Future” of Karlsruhe Institute of Technology within the framework of the German Excellence Initiative. C. Flanagan and B. Konig (Eds.): TACAS 2012, LNCS 7214, pp. 542–544, 2012. c © Springer-Verlag Berlin Heidelberg 2012 LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation 543 2 Software Architecture While LLBMC is designed for C programs, its input format is LLVM-IR, the intermediate representation of the LLVM compiler framework. LLVM-IR is an abstract assembler language that is programming-language-independent. This makes it easier to extend LLBMC to other languages supported by LLVM (like C++ or Objective-C). Furthermore, the challenges in parsing complex high-level language syntax, such as C++, are eliminated. Instead, only a limited instruction set needs to be supported. LLVM-IR is architecture-dependent in the sense that the compiler frontend selects, e.g., the bitwidth of pointers and integer data types. After reading in the LLVM-IR code, LLBMC applies a number of transformations to it. In particular, loops are unrolled, Functions are inlined, and the control flow graph is simplified. The transformed code is then converted to ILR, which is a representation of a program in the logic of bit-vectors and arrays plus some extensions, related to memory allocation. ILR provides an explicit state object for the memory content as well as for the state of the memory allocation system. These state objects encode the dependencies between memory accessing instructions in the ILR formula. Because of this, dependencies between instructions in LLVM, which were implicitly given by the ordering of the read and write operations are made explicit in the ILR formula. This change makes the expressions in an ILR formula ordering-independent. The ILR formula is then simplified using rewrite rules, and memory access correctness expressions are reduced to bit-vector formulas (see [2,7] for details). If no more rewrite rules can be applied, the formula is passed to the SMT solver STP [3]. 3 Strengths and Weaknesses of the Approach LLBMC is tailored towards finding bugs in C programs, especially memory-related ones (not so much towards proving their absence). Detectable errors include: – arithmetic overflow and underflow, including shift overflow, – invalid memory access operations, – invalid memory allocation, including invalid frees, and – overlapping memory regions in memcpy. Furthermore, LLBMC supports checking of user assertions and reachability of labels named “ERROR” in the C-code. It can also detect whether the loop unrolling and Function inlining bound was sufficient or has to be increased in order to achieve full coverage. In the competition, LLBMC was used with a fixed unwinding bound of 7 and an automatically determined Function inlining bound. It was not checked whether the unwinding bound is sufficient, but only whether the “ERROR” label was reachable within these bounds (as other comparable tools have chosen similar settings). If no error was found, the instance was considered safe. LLBMC was able to successfully handle 146 out of 269 benchmark instances (not participating in category “Concurrency”, as this is not supported by LLBMC), resulting in a first place in category “Device Drivers” and a second place in category “Heap 544 C. Sinz, F. Merz, and S. Falke Manipulation”. Among the unsolved instances, 65 were due to time-outs, and 48 due to current restrictions of LLBMC (e.g., related to memcpy or inline assembly). LLBMC produced 7 false positives and 3 false negatives. The false negatives (i.e. where an error was missed) were due to an insufficient loop unrolling bound. Among the 7 false positives, one was due to an error in LLBMC related to detecting a Malloc Function. The other 6 were due to uninitialized pointer variables, by which other (e.g., global) variables could be overwritten and thus be modified, resulting in the “ERROR” label becoming reachable. We do not consider these errors as “false positives”, but see here a special strength of LLBMC and its precise memory model, as such errors are very hard to detect and, in practice, result in non-deterministic program behavior. 4 Tool Setup and Configuration The version of LLBMC (0.9) submitted to TACAS can be downloaded from http://llbmc.org/llbmc-tacas12.zip. LLBMC requires llvm-gcc (version 2.9) in order to convert C input files to LLVM’s intermediate representation. For instructions on how to use LLBMC, just enter llbmc --help. The ZIP archive also contains two wrapper shell scripts to run LLBMC on individual C files. The first, llbmcc, iteratively increases the loop unwind bound and also checks whether the unwind bound is sufficient. The second, llbmcc2, which was used in the competition, also increases the unwind bound, but only up to a maximal value of 7, and does not perform unwind bound checks. Both shell scripts compile the C program, run LLBMC, and perform only a reachability check for a basic block labelled “ERROR”, but no other checks, such as for invalid memory accesses. They output either SAFE, if the error label is unreachable (within the given bound for llbmcc2), or UNSAFE otherwise. Further information on LLBMC is available on the web at http://llbmc.org.

Carsten Sinz - One of the best experts on this subject based on the ideXlab platform.

  • llbmc a bounded model checker for llvm s intermediate representation competition contribution
    Tools and Algorithms for Construction and Analysis of Systems, 2012
    Co-Authors: Carsten Sinz, Florian Merz, Stephan Falke
    Abstract:

    We present LLBMC, a bounded model checker for C programs. LLBMC uses the LLVM compiler framework in order to translate C programs into LLVM’s intermediate representation (IR). The resulting code is then converted into a logical representation and simplified using rewrite rules. The simplified formula is finally passed to an SMT solver. In contrast to many other tools, LLBMC uses a flat, bit-precise memory model. It can thus precisely model, e.g., memory-based re-interpret casts. 1 Verification Approach Bounded model checking (BMC) has proven to be a very successful technique in hardware verification. More recently, it has also been applied for verifying software written in C [1,4]. Applying BMC for verifying C programs, however, comes with many obstacles that have to be tackled. One of the most important differences is that the syntax and semantics of a programming language like C is much more complicated than a hardware description. One has to deal, e.g., with memory allocation and de-allocation, (Function) pointers, complex data structures, and Function calls. LLBMC uses an approach which, instead of exploring the source code directly, makes use of existing compiler technology and performs the analysis on a compiler intermediate representation. Such an intermediate representation offers a much simpler syntax and semantics than a programming language like C, and thus eases a logical encoding of the verification problem considerably. We have chosen the LLVM [5] compiler infrastructure and its assembler-like intermediate representation as the starting point for our approach, but the idea can also be applied to other low-level languages. LLVM is both a (GCC-compatible) C/C++/Objective-C compiler and a library of compiler technologies, providing, e.g., sourceand target-independent optimizations. Our primary goal is to detect memory errors in C code [7,2,6]. Memory errors include invalid memory accesses, heap and stack buffer overflows, and invalid frees (e.g., double frees). This work was supported in part by the “Concept for the Future” of Karlsruhe Institute of Technology within the framework of the German Excellence Initiative. C. Flanagan and B. Konig (Eds.): TACAS 2012, LNCS 7214, pp. 542–544, 2012. c © Springer-Verlag Berlin Heidelberg 2012 LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation 543 2 Software Architecture While LLBMC is designed for C programs, its input format is LLVM-IR, the intermediate representation of the LLVM compiler framework. LLVM-IR is an abstract assembler language that is programming-language-independent. This makes it easier to extend LLBMC to other languages supported by LLVM (like C++ or Objective-C). Furthermore, the challenges in parsing complex high-level language syntax, such as C++, are eliminated. Instead, only a limited instruction set needs to be supported. LLVM-IR is architecture-dependent in the sense that the compiler frontend selects, e.g., the bitwidth of pointers and integer data types. After reading in the LLVM-IR code, LLBMC applies a number of transformations to it. In particular, loops are unrolled, Functions are inlined, and the control flow graph is simplified. The transformed code is then converted to ILR, which is a representation of a program in the logic of bit-vectors and arrays plus some extensions, related to memory allocation. ILR provides an explicit state object for the memory content as well as for the state of the memory allocation system. These state objects encode the dependencies between memory accessing instructions in the ILR formula. Because of this, dependencies between instructions in LLVM, which were implicitly given by the ordering of the read and write operations are made explicit in the ILR formula. This change makes the expressions in an ILR formula ordering-independent. The ILR formula is then simplified using rewrite rules, and memory access correctness expressions are reduced to bit-vector formulas (see [2,7] for details). If no more rewrite rules can be applied, the formula is passed to the SMT solver STP [3]. 3 Strengths and Weaknesses of the Approach LLBMC is tailored towards finding bugs in C programs, especially memory-related ones (not so much towards proving their absence). Detectable errors include: – arithmetic overflow and underflow, including shift overflow, – invalid memory access operations, – invalid memory allocation, including invalid frees, and – overlapping memory regions in memcpy. Furthermore, LLBMC supports checking of user assertions and reachability of labels named “ERROR” in the C-code. It can also detect whether the loop unrolling and Function inlining bound was sufficient or has to be increased in order to achieve full coverage. In the competition, LLBMC was used with a fixed unwinding bound of 7 and an automatically determined Function inlining bound. It was not checked whether the unwinding bound is sufficient, but only whether the “ERROR” label was reachable within these bounds (as other comparable tools have chosen similar settings). If no error was found, the instance was considered safe. LLBMC was able to successfully handle 146 out of 269 benchmark instances (not participating in category “Concurrency”, as this is not supported by LLBMC), resulting in a first place in category “Device Drivers” and a second place in category “Heap 544 C. Sinz, F. Merz, and S. Falke Manipulation”. Among the unsolved instances, 65 were due to time-outs, and 48 due to current restrictions of LLBMC (e.g., related to memcpy or inline assembly). LLBMC produced 7 false positives and 3 false negatives. The false negatives (i.e. where an error was missed) were due to an insufficient loop unrolling bound. Among the 7 false positives, one was due to an error in LLBMC related to detecting a Malloc Function. The other 6 were due to uninitialized pointer variables, by which other (e.g., global) variables could be overwritten and thus be modified, resulting in the “ERROR” label becoming reachable. We do not consider these errors as “false positives”, but see here a special strength of LLBMC and its precise memory model, as such errors are very hard to detect and, in practice, result in non-deterministic program behavior. 4 Tool Setup and Configuration The version of LLBMC (0.9) submitted to TACAS can be downloaded from http://llbmc.org/llbmc-tacas12.zip. LLBMC requires llvm-gcc (version 2.9) in order to convert C input files to LLVM’s intermediate representation. For instructions on how to use LLBMC, just enter llbmc --help. The ZIP archive also contains two wrapper shell scripts to run LLBMC on individual C files. The first, llbmcc, iteratively increases the loop unwind bound and also checks whether the unwind bound is sufficient. The second, llbmcc2, which was used in the competition, also increases the unwind bound, but only up to a maximal value of 7, and does not perform unwind bound checks. Both shell scripts compile the C program, run LLBMC, and perform only a reachability check for a basic block labelled “ERROR”, but no other checks, such as for invalid memory accesses. They output either SAFE, if the error label is unreachable (within the given bound for llbmcc2), or UNSAFE otherwise. Further information on LLBMC is available on the web at http://llbmc.org.

Florian Merz - One of the best experts on this subject based on the ideXlab platform.

  • llbmc a bounded model checker for llvm s intermediate representation competition contribution
    Tools and Algorithms for Construction and Analysis of Systems, 2012
    Co-Authors: Carsten Sinz, Florian Merz, Stephan Falke
    Abstract:

    We present LLBMC, a bounded model checker for C programs. LLBMC uses the LLVM compiler framework in order to translate C programs into LLVM’s intermediate representation (IR). The resulting code is then converted into a logical representation and simplified using rewrite rules. The simplified formula is finally passed to an SMT solver. In contrast to many other tools, LLBMC uses a flat, bit-precise memory model. It can thus precisely model, e.g., memory-based re-interpret casts. 1 Verification Approach Bounded model checking (BMC) has proven to be a very successful technique in hardware verification. More recently, it has also been applied for verifying software written in C [1,4]. Applying BMC for verifying C programs, however, comes with many obstacles that have to be tackled. One of the most important differences is that the syntax and semantics of a programming language like C is much more complicated than a hardware description. One has to deal, e.g., with memory allocation and de-allocation, (Function) pointers, complex data structures, and Function calls. LLBMC uses an approach which, instead of exploring the source code directly, makes use of existing compiler technology and performs the analysis on a compiler intermediate representation. Such an intermediate representation offers a much simpler syntax and semantics than a programming language like C, and thus eases a logical encoding of the verification problem considerably. We have chosen the LLVM [5] compiler infrastructure and its assembler-like intermediate representation as the starting point for our approach, but the idea can also be applied to other low-level languages. LLVM is both a (GCC-compatible) C/C++/Objective-C compiler and a library of compiler technologies, providing, e.g., sourceand target-independent optimizations. Our primary goal is to detect memory errors in C code [7,2,6]. Memory errors include invalid memory accesses, heap and stack buffer overflows, and invalid frees (e.g., double frees). This work was supported in part by the “Concept for the Future” of Karlsruhe Institute of Technology within the framework of the German Excellence Initiative. C. Flanagan and B. Konig (Eds.): TACAS 2012, LNCS 7214, pp. 542–544, 2012. c © Springer-Verlag Berlin Heidelberg 2012 LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation 543 2 Software Architecture While LLBMC is designed for C programs, its input format is LLVM-IR, the intermediate representation of the LLVM compiler framework. LLVM-IR is an abstract assembler language that is programming-language-independent. This makes it easier to extend LLBMC to other languages supported by LLVM (like C++ or Objective-C). Furthermore, the challenges in parsing complex high-level language syntax, such as C++, are eliminated. Instead, only a limited instruction set needs to be supported. LLVM-IR is architecture-dependent in the sense that the compiler frontend selects, e.g., the bitwidth of pointers and integer data types. After reading in the LLVM-IR code, LLBMC applies a number of transformations to it. In particular, loops are unrolled, Functions are inlined, and the control flow graph is simplified. The transformed code is then converted to ILR, which is a representation of a program in the logic of bit-vectors and arrays plus some extensions, related to memory allocation. ILR provides an explicit state object for the memory content as well as for the state of the memory allocation system. These state objects encode the dependencies between memory accessing instructions in the ILR formula. Because of this, dependencies between instructions in LLVM, which were implicitly given by the ordering of the read and write operations are made explicit in the ILR formula. This change makes the expressions in an ILR formula ordering-independent. The ILR formula is then simplified using rewrite rules, and memory access correctness expressions are reduced to bit-vector formulas (see [2,7] for details). If no more rewrite rules can be applied, the formula is passed to the SMT solver STP [3]. 3 Strengths and Weaknesses of the Approach LLBMC is tailored towards finding bugs in C programs, especially memory-related ones (not so much towards proving their absence). Detectable errors include: – arithmetic overflow and underflow, including shift overflow, – invalid memory access operations, – invalid memory allocation, including invalid frees, and – overlapping memory regions in memcpy. Furthermore, LLBMC supports checking of user assertions and reachability of labels named “ERROR” in the C-code. It can also detect whether the loop unrolling and Function inlining bound was sufficient or has to be increased in order to achieve full coverage. In the competition, LLBMC was used with a fixed unwinding bound of 7 and an automatically determined Function inlining bound. It was not checked whether the unwinding bound is sufficient, but only whether the “ERROR” label was reachable within these bounds (as other comparable tools have chosen similar settings). If no error was found, the instance was considered safe. LLBMC was able to successfully handle 146 out of 269 benchmark instances (not participating in category “Concurrency”, as this is not supported by LLBMC), resulting in a first place in category “Device Drivers” and a second place in category “Heap 544 C. Sinz, F. Merz, and S. Falke Manipulation”. Among the unsolved instances, 65 were due to time-outs, and 48 due to current restrictions of LLBMC (e.g., related to memcpy or inline assembly). LLBMC produced 7 false positives and 3 false negatives. The false negatives (i.e. where an error was missed) were due to an insufficient loop unrolling bound. Among the 7 false positives, one was due to an error in LLBMC related to detecting a Malloc Function. The other 6 were due to uninitialized pointer variables, by which other (e.g., global) variables could be overwritten and thus be modified, resulting in the “ERROR” label becoming reachable. We do not consider these errors as “false positives”, but see here a special strength of LLBMC and its precise memory model, as such errors are very hard to detect and, in practice, result in non-deterministic program behavior. 4 Tool Setup and Configuration The version of LLBMC (0.9) submitted to TACAS can be downloaded from http://llbmc.org/llbmc-tacas12.zip. LLBMC requires llvm-gcc (version 2.9) in order to convert C input files to LLVM’s intermediate representation. For instructions on how to use LLBMC, just enter llbmc --help. The ZIP archive also contains two wrapper shell scripts to run LLBMC on individual C files. The first, llbmcc, iteratively increases the loop unwind bound and also checks whether the unwind bound is sufficient. The second, llbmcc2, which was used in the competition, also increases the unwind bound, but only up to a maximal value of 7, and does not perform unwind bound checks. Both shell scripts compile the C program, run LLBMC, and perform only a reachability check for a basic block labelled “ERROR”, but no other checks, such as for invalid memory accesses. They output either SAFE, if the error label is unreachable (within the given bound for llbmcc2), or UNSAFE otherwise. Further information on LLBMC is available on the web at http://llbmc.org.

Dávila Foyo Diego - One of the best experts on this subject based on the ideXlab platform.

  • Optimization of a parallel Monte Carlo method for linear algebra problems
    Universitat Politècnica de Catalunya, 2016
    Co-Authors: Dávila Foyo Diego
    Abstract:

    Many problems in science and engineering can be represented by Systems of Linear Algebraic Equations (SLAEs). Numerical methods such as direct or iterative ones are used to solve these kind of systems. Depending on the size and other factors that characterize these systems they can be sometimes very difficult to solve even for iterative methods, requiring long time and large amounts of computational resources. In these cases a preconditioning approach should be applied. Preconditioning is a technique used to transform a SLAE into a equivalent but simpler system which requires less time and effort to be solved. The matrix which performs such transformation is called the preconditioner [7]. There are preconditioners for both direct and iterative methods but they are more commonly used among the later ones. In the general case a preconditioned system will require less effort to be solved than the original one. For example, when an iterative method is being used, less iterations will be required or each iteration will require less time, depending on the quality and the efficiency of the preconditioner. There are different classes of preconditioners but we will focused only on those that are based on the SParse Approximate Inverse (SPAI) approach. These algorithms are based on the fact that the approximate inverse of a given SLAE matrix can be used to approximate its result or to reduce its complexity. Monte Carlo methods are probabilistic methods, that use random numbers to either simulate a stochastic behaviour or to estimate the solution of a problem. They are good candidates for parallelization due to the fact that many independent samples are used to estimate the solution. These samples can be calculated in parallel, thereby speeding up the solution finding process [27]. In the past there has been a lot of research around the use of Monte Carlo methods to calculate SPAI preconditioners [1] [27] [10]. In this work we present the implementation of a SPAI preconditioner that is based on a Monte Carlo method. This algorithm calculates the matrix inverse by sampling a random variable which approximates the Neumann Series expansion. Using the Neumman series it is possible to calculate the matrix inverse of a system A by performing consecutive additions of the powers of a matrix expressed by the series expansion of (I − A) −1 . Given the stochastic approach of the Monte Carlo algorithm, the computational effort required to find an element of the inverse matrix is independent from the size of the matrix. This allows to target systems that, due to their size, can be prohibitive for common deterministic approaches [27]. Great part of this work is focused on the enhancement of this algorithm. First, the current errors of the implementation were fixed, making the algorithm able to target larger systems. Then multiple optimizations were applied at different stages of the implementation making a better use of the resources and improving the performance of the algorithm. Four optimizations, with consistently improvements have been performed: 1. An inefficient implementation of the realloc Function within the MPI library was provoking the application to rapidly run out of memory. This Function was replaced by the Malloc Function and some slight modifications to estimate the size of matrix A. 2. A coordinate format (COO) was introduced within the algorithm’s core to make a more efficient use of the memory, avoiding several unnecessary memory accesses. 3. A method to produce an intermediate matrix P was shown to produce similar results to the default one and with matrix P being reduced to a single vector, thus requiring less data. Given that this was a broadcast data a diminishing on it, translated into a reduction of the broadcast time. 4. Four individual procedures which accessed the whole initial matrix memory, were merged into two processes, reducing this way the number of memory accesses. For each optimization applied, a comparison was performed to show the particular improvements achieved. A set of different matrices, representing different SLAEs, was used to show the consistency of these improvements. In order to provide with insights about the scalability issues of the algorithm, other approaches are presented to show the particularities of the algorithm’s scalability: 1. Given that the original version of this algorithm was designed for a cluster of single-core machines, an hybrid approach of MPI + openMP was proposed to target the nowadays multi-core architectures. Surprisingly this new approach did not show any improvement but it was useful to show a scalability problem related to the random pattern used to access the memory. 2. Having that common MPI implementations of the broadcast operation do not take into account the different latencies between inter-node and intra-node communications [25]. Therefore, we decided to implement the broadcast in two steps. First by reaching a single process in each of the compute nodes and then using those processes to perform a local broadcast within their compute nodes. Results on this approach showed that this method could lead to improvements when very big systems are used. Finally a comparison is carried out between the optimized version of the Monte Carlo algorithm and the state of the art Modified SPAI (MSPAI). Four metrics are used to compare these approaches: 1. The amount of time needed for the preconditioner construction. 2. The time needed by the solver to calculate the solution of the preconditioned system. 3. The addition of the previous metrics, which gives a overview of the quality and efficiency of the preconditioner. 4. The number of cores used in the preconditioner construction. This gives an idea of the energy efficiency of the algorithm. Results from previous comparison showed that Monte Carlo algorithm can deal with both symmetric and nonsymmetric matrices while MSPAI only performs well with the nonsymetric ones. Furthermore the time for Monte Carlo’s algorithm is always faster for the preconditioner construction and most of the times also for the solver calculation. This means that Monte Carlo produces preconditioners of better or same quality than MSPAI. Finally, the number of cores used in the Monte Carlo approach is always equal or smaller than in the case of MSPAI