Microsoft Technology Licensing, LLC

Other

Shaz Qadeer

Madanlal S Musuvathi

Sriram K Rajamani

Niels Jakob Rehof

Rui Wang

Shuo Chen

Yuri Gurevich

Akash Lal

Yuchen Zhou

Narayanan Ganapathy

Anthony Dean Andrews

Robert Anthony DeLine

Shuvendu K Lahiri

Jeremy P Condit

Vladimir A Levin

Mike Barnett

Dinghao Wu

Tayfun Elmas

Robert Palmer

Yichen Xie

Alastair Francis Donaldson

Jacob Samuels Burnim

A framework is described herein for identifying implicit assumptions associated with an SDK and its accompanying documentation (e.g., dev guide). An implicit assumption is information that is not expressly stated in the documentation, but which would be useful in assisting an application developer in building an application. The framework also describes a systematic approach for identifying one or more vulnerability patterns based on the identified implicit assumptions. An application developer may run a test on an application that is being developed to ensure that it does not have any deficiency which matches a vulnerability pattern.

Identifying implicit assumptions associated with a software product

In various embodiments, methods and systems for testing failover and recovery are provided. Systematic testing of a distributed system is performed, where the systematic testing probabilistically determines a processing order of events to effectuate system states for the plurality of state machines. An iteration of the systematic testing tests one the system states and includes sending a termination message to a state machine; receiving a termination acknowledgment message, the termination message causing the state machine to halt at the state and event of the state machine for the system state; and instantiating a recovery state machine. The recovery state machine is instantiated with a same state and same role as the halted state machine. Results of the systematic testing are verified against an expected outcome, the results being generated by running the distributed system with the instantiated recovery state machine for each iteration of the systematic testing.

Systematic testing of failover and recovery for distributed system components

A symbolic encoding of predicated execution for static verification, based on a plurality of data parallel program instructions, is obtained. A result of static verification of one or more attributes associated with the plurality of data parallel program instructions is obtained, based on the symbolic encoding.

Static verification of parallel program code

Techniques for providing a fair stateless model checker are disclosed. In some aspects, a schedule is generated to allocate resources for threads of a multi-thread program in lieu of having an operating system allocate resources for the threads. The generated schedule is both fair and exhaustive. In an embodiment, a priority graph may be implemented to reschedule a thread when a different thread is determined not to be making progress. A model checker may then implement one of the generated schedules in the program in order to determine if a bug or a livelock occurs during the particular execution of the program. An output by the model checker may facilitate identifying bugs and/or livelocks, or authenticate a program as operating correctly.

Fair stateless model checking

A concurrency assertions system disclosed herein provides for atomic evaluation of an assertion expression by locking an assertion lock upon initiating an assertion and thereby protecting the assertion evaluation from concurrent modifications to the variables in the assertion expressions. When a violation of an assertion is detected, the concurrency assertions system ensures that the exception statistics at the time of the assertion violation represents a program state where the assertion is violated, thus improving analysis of assertion violations. Furthermore, the concurrency assertions system continuously evaluates an expression for an assertion for a time period while other threads in the program are being executed.

Concurrent assertion

Various technologies pertaining to answering reachability queries are described herein. A reachability query includes a user-specified destination line of code in source code that is desirably analyzed. A theorem prover is employed to identify an execution path through the source code that reaches the destination line of code. Graphical data is presented to the user that illustrates to the user the execution path through the source code that reaches the destination line of code.

Identifying execution paths that satisfy reachability queries

This document describes a unified type checker and property checker for a low level program's heap and its types. The type checker can use the full power of the property checker to express and verify subtle, program specific type and memory safety invariants well beyond what the native low level program system can check. Meanwhile, the property checker can rely on the type checker to provide structure and disambiguation for the program's heap, enabling more concise and more powerful type-based specifications. This approach makes use of a fully automated Satisfiability Modulo Theories (SMT) solver and a decision procedure for checking type safety, which means that the programmer's only duty is to provide high-level type and property annotations as part of the original program's source.

Unifying type checking and property checking for low level programs

Testing multithreaded application programs for errors can be carried out in an efficient and productive manner at least in part by prioritizing thread schedules based on numbers of context switches between threads therein. In particular, each thread schedule in a multithreaded application program can be prioritized based on whether a given thread schedule has the same as or less than some maximum value. A model checker module can then iteratively execute thread schedules that fit within a given context switch maximum value, or a progressively higher value up to some limit. In one implementation, for example, the model checker module executes all thread schedules that have zero preempting context switches, then all thread schedules that have only one preempting context switch, etc. Most errors in an application program can be identified by executing only those thread schedule with relatively few preempting context switches.

Testing multi-thread software using prioritized context switch limits

Validity of one or more assertions for any concurrent execution of a plurality of software instructions with at most k&#x2212;1 context switches can be determined. Validity checking can account for execution of the software instructions in an unbounded stack depth scenario. A finite data domain representation can be used. The software instructions can be represented by a pushdown system. Validity checking can account for thread creation during execution of the plurality of software instructions.

Model checking with bounded context switches

A data race detection system is described which precisely identifies data races in concurrent programs. The system and techniques described utilize locksets to maintain information while searching through executions of a concurrent program. The locksets are updated according to program statements in the concurrent program. The dynamic updating of the locksets, combined with a less conservative approach then used in existing lockset data race detection techniques, allows the technique to be precise; that is, the technique does not report false positives when searching a program.

Precise data-race detection using locksets

Described techniques and tools help model checking scale to large programs while reducing missed errors. In particular, described techniques and tools help reduce the state space of concurrent programs without depending on cycle detection and without scheduling execution of postponed threads at all cycles. For example, described techniques and tools use a type of partial-order reduction called transaction-based reduction to reduce program state space. Analysis is performed at commit points to determine whether to schedule delayed threads.

Sound transaction-based reduction without cycle detection

Procedure summaries can be generated and used for multithreaded software. A set of actions for a software procedure can be identified as atomically modelable with respect to multithreaded execution of the software. Such actions can be considered a transaction and deemed to have occurred one after another without interruption by other threads. Thus, multithreaded execution of the software can be modeled to detect programming flaws. For example, reachability analysis can be used in concert with the procedure summaries to determine if specified invariants fail.

Procedure summaries for multithreaded software

The state space of modeled software can be explored using an object-based systematic state explorer. The object-based model can perform well even in light of the complexities of concurrent software. During state space exploration, differences between states can be stored instead of storing a complete copy of the state.

Object-based systematic state space exploration of software

A concurrent program is analyzed for the presence of data races by the creation of a sequential program from the concurrent program. The sequential program contains assertions which can be verified by a sequential program analysis tool, and which, when violated, indicate the presence of a data race. The sequential program emulates multiple executions of the concurrent program by nondeterministically scheduling asynchronous threads of the concurrent program on a single runtime stack and nondeterministically removing the currently-executing thread from the stack before instructions of the program. Checking functions are used to provide assertions for data races, along with a global access variable, which indicates if a variable being analyzed for data races is currently being accessed by any threads.

Growing community of inventors

Seattle, WA, United States of America

Shaz Qadeer