Fair stateless model checking
US9063778B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jan 9, 2008 |
| Grant date | Jun 23, 2015 |
| Priority date | — |
| Expiry date | Sep 15, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F2209/484
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.