Methods, systems, and media for providing determinism in multithreaded programs

• US 9,454,460 B2
• Filed: 07/25/2011
• Issued: 09/27/2016
• Est. Priority Date: 07/23/2010
• Status: Expired due to Fees

• 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
• Primary Examiner(s): LOUIE, JUE WANG
• Application Number:
  US13/190,316
• Publication Number:
  US 20120102470A1
• Time in Patent Office: 1,891 Days
• Field of Search: None
• US Class Current: 1/1
• 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 the multithreaded program executed by a hardware processor with;

a proxy that;

receives first inputs to the multithreaded program; and

determines whether a schedule of execution of a plurality of threads in the multithreaded program corresponding to a set of input constraints satisfied by the first inputs has been memoized, wherein the set of input constraints is satisfied by a plurality of inputs to the multithreaded program including the first inputs and second inputs, wherein the second inputs are different than the first inputs; and

a replayer that;

if it is determined that the schedule corresponding to the set of input constraints satisfied by the first inputs has been memoized, processes the first inputs by the multithreaded 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 first 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 first 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 first 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 input constraints based on a reuse rate of each of the plurality of schedules.

19. The method of claim 1, wherein processing the first 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 first inputs to the multithreaded program;

determining whether a schedule of execution of a plurality of threads in the multithreaded program corresponding to a set of input constraints satisfied by the first inputs has been memoized, wherein the set of input constraints is satisfied by a plurality of inputs to the multithreaded program including the first inputs and second inputs, wherein the second inputs are different than the first inputs; and

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