Methods, Systems, and Media for Providing Determinism in Multithreaded Programs

• US 20120102470A1
• Filed: 07/25/2011
• Published: 04/26/2012
• Est. Priority Date: 07/23/2010
• Status: Active Grant

• Current Assignee: Trustees Of Columbia University In The City Of New York (Columbia University)
• Original Assignee: Trustees Of Columbia University In The City Of New York (Columbia University)
• Inventors: Yang, Junfeng, Cui, Heming, Wu, Jingyue
• Granted Patent: US 9,454,460 B2
• Time in Patent Office: Days
• US Class Current: 717/130
• CPC Class Codes: G06F 11/3632 of specific synchronisation aspects
• CPC Class Codes: G06F 8/458 Synchronisation, e.g. post-wait, barriers, locks synchronisation among tasks G06F9/52

Abstract

Methods, systems, and media for providing determinism in multithreaded programs are provided. In some embodiments, methods for providing determinism in multithreaded programs are provided, the methods comprising: instrumenting a program with: a proxy that: receives inputs to the program; and determines whether a schedule corresponding to a set of input constraints satisfied by the inputs has been memoized; and a replayer that: if it is determined that a schedule corresponding to a set of input constraints satisfied by the inputs has been memoized, processes the inputs by the program according to the schedule.

Claims

1. A method for providing determinism in a multithreaded program, comprising:

instrumenting a program with;

a proxy that;

receives inputs to the program; and

determines whether a schedule corresponding to a set of input constraints satisfied by the inputs has been memoized; and

a replayer that;

if it is determined that a schedule corresponding to a set of input constraints satisfied by the inputs has been memoized, processes the inputs by the program according to the schedule.

2. The method of claim 1, further comprising also instrumenting the program with a memoizer that:

records synchronization operations into the schedule;

determines the set of input constraints corresponding to the schedule; and

stores the schedule.

3. The method of claim 2, wherein the memoizer also determines if races are present in the schedule.

4. The method of claim 3, wherein the races are data races.

5. The method of claim 3, wherein the races are schedule races.

6. The method of claim 2, wherein the inputs are requests and wherein the memoizer also buffers the requests in a window before recording the synchronization operations into the schedule.

7. The method of claim 2, wherein the memoizer records, determines the set of input constraints, and stores asynchronously of an execution of the program.

8. The method of claim 2, wherein the memoizer also tracks constraints on marked symbolic data.

9. The method of claim 8, wherein tracking constraints includes at least one of:

tracking data that is derived from the marked symbolic data;

tracking outcomes of branch statements that observe the marked symbolic data; and

tracking outcomes of branch statements that observe the data is derived from the marked symbolic data.

10. The method of claim 2, wherein the schedules are stored by a constraint-schedule tuple.

11. The method of claim 2, wherein the schedules are stored as a decision tree.

12. The method of claim 2, wherein the memoizer also determines whether a schedule includes a symbolic race;

and if a symbolic race is determined to be included in the schedule, adds additional input constraints to the set of input constraints to prevent the symbolic race in reuse of the schedule.

13. The method of claim 2, wherein the memoizer also simplifies the set of input constraints.

14. The method of claim 2, wherein the memoizer also ignores branch statements that are unlikely to affect synchronization operations.

15. The method of claim 1, wherein the inputs are requests and wherein at least one of the proxy and the replayer buffer the requests in a window before the requests are processed.

16. The method of claim 1, wherein the proxy determines whether a schedule corresponding to a set of input constraints satisfied by the inputs has been memoized comprising checking a prepopulated cache of memoized schedules.

17. The method of claim 1, wherein the program is instrumented to include at least one of marking of data that may affect schedules;

marking of the beginning and the end of logical tasks;

annotating of synchronization operations;

annotating of blocking system calls; and

annotating of hidden states.

18. The method of claim 1, wherein at least one of the proxy and the replayer selects the schedule from a plurality of schedules with the set of inputs constraints based on a reuse rate of each the plurality schedules.

19. The method of claim 1, wherein processing the inputs by the program according to the schedule comprises:

assigning a first semaphore to a first thread of the program;

assigning a second semaphore to a second thread of the program;

causing the first thread to wait for the first semaphore to indicate that the first thread can run;

when the first semaphore indicates that the first thread can run, running the first thread;

causing the second thread to wait for the second semaphore to indicate that the second thread can run; and

causing the second semaphore to indicate that the second thread can run when the first thread has finished running.

20. A method for providing determinism in a multithreaded program, comprising:

receiving inputs to a program;

determining whether a schedule corresponding to a set of input constraints satisfied by the inputs has been memoized; and

if it is determined that a schedule corresponding to a set of input constraints satisfied by the inputs has been memoized, processing the inputs by the program according to the schedule.