International Business Machines Corporation

Rachel Tzoref

Shmuel Ur

Aviad Zlotnick

Ohad Shacham

Daniel Geist

Ehud Trainin

Mark Ginzburg

Yoad Lustig

Ishai Rabinovitz

Yarden Nir-Buchbinder

Eitan D Farchi

Yaakov Yaari

Elad Yom-Tov

Onn Menahem Shehory

Moshe Klausner

Maayan Goldstein

Orna Raz-Pelleg

Yousef Shajrawi

Aharon Kupershtok

Ishai Rabinovotz

A computer implemented system and method for measuring synchronization coverage for one or more concurrently executed threads is provided. The method comprises updating an identifier of a first thread to comprise an operation identifier associated with a first operation, in response to determining that the first thread has performed the first operation; associating the identifier of the first thread with one or more resources accessed by the first thread; and generating a synchronization coverage model by generating a relational data structure of said one or more resources, wherein a resource is associated with at least the identifier of the first thread and an identifier of a second thread identifier, such that the second thread waits for the first thread before accessing said resource.

Verifying synchronization coverage in logic code

Detecting optimization opportunities is enabled by utilizing a trace of a target concurrent computer program and determining a relation between data objects accessed during the tracked execution. The relation may be stored in a Temporal Relation Graph (TRG), in an extended-TRG or another data structure. The relation may be affected by temporally-adjacent accesses to data objects. The relation may further be affected by accesses to data objects performed during critical sections of the target program.

Performance optimization based on data accesses during critical sections

A computer-implemented method is provided, including monitoring one or more parameters of a computer system that executes one or more service requester processes that issue service requests to one or more service provider processes. A congestion in the system is detected by analyzing the parameters. Upon identifying at least one of the service requester processes as contributing to the congestion, execution of the at least one of the service requester processes is slowed. Other embodiments are also described.

Congestion control using application slowdown

A method for enhancing synchronization coverage for a logic code is provided. The method comprises tracking whether one or more code sections in the logic code are blocked by at least another code section in the logic code, or whether one or more code sections in the logic code are blocking at least another code section in the logic code, during one or more test runs; and including one or more delay mechanisms in the logic code to introduce a delay in execution of a first code section in the logic code, wherein length of introduced delay is dependent on whether the first code section was blocked by a second code section or whether the first code section was blocking the second code section.

Synchronization coverage in logic code

Systems and methods that use a solver to find bugs in a target model of a computing system having one or more finite computation paths are provided. The bugs on computation paths of less than a predetermined length are detected by translating the target model to include a state variable AF for one or more states of the target model, wherein AF(S) represents value of the state variable AF at state S; and solving the translated version of the target model that satisfies predetermined constrains.

Satisfiability (SAT) based bounded model checkers

Detecting locking discipline violations on shared resources. For example, a method of detecting locking discipline violations of shared resources of a computing platform, by a testing process to be executed concurrently with one or more other processes on said computing platform, the testing process comprising: locking a shared resource of said computing platform; reading a value of the shared resource; locally storing the value of the shared resource; rereading the value of the shared resource after a predefined time period; and generating a locking discipline violation report if the value of said shared resource as reread by said rereading is different from the value of said resource as locally stored by said locally storing.

Detecting locking discipline violations on shared resources

Device, system, and method of debugging computer programs. For example, a method for debugging computer programs includes: locating a bug in a computer program based on a first score corresponding to a first instrumentation location of the computer program and a second score corresponding to a second instrumentation location of the computer program.

Device, system and method of debugging computer programs

A method uses a SAT solver operating to cycle k to find bugs in a model having finite computation paths therein, wherein said bugs are on computation paths of less than length k. Another method includes adding an additional state variable to a model to be checked, where a governing state machine of the additional variable has a 'sink' state. The method includes having a translation using the additional variable whenever a state indicates a bad state and performing satisfiability solving with the model and the translation.

A method for preventing deadlocks in a multiprocessing environment is provided. The method comprises receiving one or more strongly connected components (SCCs) as input, wherein a first SCC represents a set of locks such that each pair of locks in the set may potentially be involved in a deadlock situation; creating a first gate lock for the first SCC, wherein a first process or process element acquires the first gate lock before acquiring a first lock in the first SCC and releases the first gate lock after releasing a number of locks in the first SCC; and removing the first gate lock, in response to determining that the first gate lock introduces new deadlocks.

Growing community of inventors

Haifa, Israel

Rachel Tzoref