Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
- Publication Type
Articles 1 - 13 of 13
Full-Text Articles in Physical Sciences and Mathematics
Zipperotf: Automatic, Precise, And Simple Data Race Detection For Task Parallel Programs With Mutual Exclusion, S. Jacob Powell
Zipperotf: Automatic, Precise, And Simple Data Race Detection For Task Parallel Programs With Mutual Exclusion, S. Jacob Powell
Theses and Dissertations
Data race in parallel programs can be difficult to precisely detect, and doing so manually can often prove unsuccessful. Task parallel programming models can help reduce defects introduced by the programmer by restricting concurrent functionalities to fork-join operations. Typical data race detection algorithms compute the happens-before relation either by tracking the order that shared accesses happen via a vector clock counter, or by grouping events into sets that help classify which heap locations are accessed sequentially or in parallel. Access sets are simple and efficient to compute, and have been shown to have the potential to outperform vector clock approaches …
Verification Of Task Parallel Programs Using Predictive Analysis, Radha Vi Nakade
Verification Of Task Parallel Programs Using Predictive Analysis, Radha Vi Nakade
Theses and Dissertations
Task parallel programming languages provide a way for creating asynchronous tasks that can run concurrently. The advantage of using task parallelism is that the programmer can write code that is independent of the underlying hardware. The runtime determines the number of processor cores that are available and the most efficient way to execute the tasks. When two or more concurrently executing tasks access a shared memory location and if at least one of the accesses is for writing, data race is observed in the program. Data races can introduce non-determinism in the program output making it important to have data …
An Analyzer For Message Passing Programs, Yu Huang
An Analyzer For Message Passing Programs, Yu Huang
Theses and Dissertations
Asynchronous message passing systems are fast becoming a common means for communication between devices. Two problems existing in message passing programs are difficult to solve. The first problem, intended or otherwise, is message-race where a receive may match with more than one send in the runtime system. This non-determinism often leads to intermittent and unexpected behavior depending on the resolution of the race. Another problem is deadlock, which is a situation in that each member process of the group is waiting for some member process to communicate with it, but no member is attempting to communicate with it. Detecting if …
Test Case Generation Using Model Checking For Software Components Deployed Into New Environments, Tonglaga Bao, Michael D. Jones
Test Case Generation Using Model Checking For Software Components Deployed Into New Environments, Tonglaga Bao, Michael D. Jones
Faculty Publications
In this paper, we show how to generate test cases for a component deployed into a new software environment. This problem is important for software engineers who need to deploy a component into a new environment. Most existing model based testing approaches generate models from high level specifications. This leaves a semantic gap between the high level specification and the actual implementation. Furthermore, the high level specification often needs to be manually translated into a model, which is a time consuming and error prone process. We propose generating the model automatically by abstracting the source code of the component using …
Verifying Abstract Components Within Concrete Software Environments, Tonglaga Bao
Verifying Abstract Components Within Concrete Software Environments, Tonglaga Bao
Theses and Dissertations
In order to model check a software component which is not a standalone program, we need a model of the software which completes the program. This problem is important for software engineers who need to deploy an existing component into a new environment. The model is typically generated by abstracting the surrounding software environment in which the component will be executed. However, abstracting the surrounding software is a difficult and error-prone task, particularly when the surrounding software is a complex software artifact which can not be easily abstracted. In this dissertation, we present a new approach to the problem by …
Using Live Sequence Chart Specifications For Formal Verification, Rahul Kumar
Using Live Sequence Chart Specifications For Formal Verification, Rahul Kumar
Theses and Dissertations
Formal methods play an important part in the development as well as testing stages of software and hardware systems. A significant and often overlooked part of the process is the development of specifications and correctness requirements for the system under test. Traditionally, English has been used as the specification language, which has resulted in verbose and difficult to use specification documents that are usually abandoned during product development. This research focuses on investigating the use of Live Sequence Charts (LSCs), a graphical and intuitive language directly suited for expressing communication behaviors of a system as the specification language for a …
Machine Code Verification Using The Bogor Framework, Joseph R. Edelman
Machine Code Verification Using The Bogor Framework, Joseph R. Edelman
Theses and Dissertations
Verification and validation of embedded systems software is tedious and time consuming. Software model checking uses a tool-based approach automating this process. In order to more accurately model software it is necessary to provide hardware support that enables the execution of software as it should run on native hardware. Hardware support often requires the creation of model checking tools specific to the instruction set architecture. The creation of software model checking tools is non-trivial. We present a strategy for using an "off-the-shelf" model checking tool, Bogor, to provide support for multiple instruction set architectures. Our strategy supports key hardware features …
Finding Termination And Time Improvement In Predicate Abstraction With Under-Approximation And Abstract Matching, Dritan Kudra
Finding Termination And Time Improvement In Predicate Abstraction With Under-Approximation And Abstract Matching, Dritan Kudra
Theses and Dissertations
The focus of current formal verification methods is mitigating the state explosion problem. One of these formal methods is predicate abstraction, which reduces concrete states of a system to bitvectors of true/false valuations of a set of predicates. Predicate abstraction comes in two flavors, over-approximation and under-approximation. A drawback of over-approximation is that it produces too many spurious errors for data-intensive applications. A more recent under-approximation technique which does not produce spurious errors, does abstract matching on concrete states (AMCS). AMCS adds behaviors to an abstract system by augmenting the set of initial predicates, making use of a theorem prover. …
On-The-Fly Dynamic Dead Variable Analysis, Joel P. Self
On-The-Fly Dynamic Dead Variable Analysis, Joel P. Self
Theses and Dissertations
State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover …
Improving Error Discovery Using Guided Model Checking, Neha Shyam Rungta
Improving Error Discovery Using Guided Model Checking, Neha Shyam Rungta
Theses and Dissertations
State exploration in directed software model checking is guided using a heuristic function to move states near errors to the front of the search queue. Distance heuristic functions rank states based on the number of transitions needed to move the current program state into an error location. Lack of calling context information causes the heuristic function to underestimate the true distance to the error; however, inlining functions at call sites in the control flow graph to capture calling context leads to exponential growth in the computation. This paper presents a new algorithm that implicitly inlines functions at call sites to …
A Context-Sensitive Structural Heuristic For Guided Search Model Checking, Eric G. Mercer, Neha Rungta
A Context-Sensitive Structural Heuristic For Guided Search Model Checking, Eric G. Mercer, Neha Rungta
Faculty Publications
Software verification using model checking often translates programs into corresponding transition systems that model the program behavior. As software systems continue to grow in complexity and size, exhaustively checking a property on a transition graph becomes difficult. The goal of guided search heuristics in model checking is to find a counterexample to the property being verified as quickly as possible in the transition graph. The FSM distance heuristic builds an interprocedural control flow graph of the program to estimate distance to a possible error state. It ignores calling context and underestimates the true distance to the error.
Dynamic Dead Variable Analysis, Micah S. Lewis
Dynamic Dead Variable Analysis, Micah S. Lewis
Theses and Dissertations
Dynamic dead variable analysis (DDVA) extends traditional static dead variable analysis (SDVA) in the context of model checking through the use of run-time information. The analysis is run multiple times during the course of model checking to create a more precise set of dead variables. The DDVA is evaluated based on the amount of memory used to complete model checking relative to SDVA while considering the extra overhead required to implement DDVA. On several models with a complex control flow graph, DDVA reduces the amount of memory needed by 38-88MB compared to SDVA with a cost of 36 bytes of …
January: Search Based On Social Insect Behavior, Peter C. Lamborn
January: Search Based On Social Insect Behavior, Peter C. Lamborn
Theses and Dissertations
January is a group of interacting stateless model checkers. Each agent functions on a processor located on a super computer or a network of workstations (NOW). The agent's search pattern is a semi-random walk based on the behavior of the grey field slug (Agriolimax reticulatus), the house fly (Musca domestica), and the black ant (Lassius niger). The agents communicate to lessen the amount of duplicate work being done. Every algorithm has a memory threshold above which they search efficiently. This threshold varies not only by model but also by algorithm. Janaury's threshold is lower than the thresholds of other algorithms …