- 专利标题: DYNAMIC SYNTHESIS OF PROGRAM SYNCHRONIZATION
-
申请号: US13418900申请日: 2012-03-13
-
公开(公告)号: US20130247000A1公开(公告)日: 2013-09-19
- 发明人: Martin Vechev , Eran Yahav
- 申请人: Martin Vechev , Eran Yahav
- 申请人地址: US NY Armonk
- 专利权人: INTERNATIONAL BUSINESS MACHINE CORPORATION
- 当前专利权人: INTERNATIONAL BUSINESS MACHINE CORPORATION
- 当前专利权人地址: US NY Armonk
- 主分类号: G06F9/44
- IPC分类号: G06F9/44
摘要:
Dynamic synthesis includes receiving a program P and a specification S that describes desired properties of P. The dynamic synthesis also includes initializing a constraint C to true, enumerating schedules up to a defined limit that satisfy C, and executing a schedule of P. The dynamic synthesis further includes determining whether execution of the schedule violates S. In response to determining that the execution violates S, the dynamic synthesis includes determining whether to avoid future executions of the schedule. In response to determining that future executions of the schedule should be avoided, the dynamic synthesis includes computing a constraint that avoids the future execution, and adding the constraint to C; otherwise, the dynamic synthesis includes selecting another schedule for execution. In response to determining that the execution of the schedule does not violate S, the dynamic synthesis includes selecting another schedule for execution.
信息查询