专利快速检索-快速检索全球专利，免费商用专利数据库-IPRDB

11. 发明申请

US20060248515A1 Sound transaction-based reduction without cycle detection 有权
标题翻译：基于声音的基于事务的减少，无周期检测
公开(公告)号：US20060248515A1
公开(公告)日：2006-11-02
申请号：US11119530
申请日：2005-04-29
申请人： Shaz Qadeer , Sriram Rajamani , Vladimir Levin , Robert Palmer
发明人： Shaz Qadeer , Sriram Rajamani , Vladimir Levin , Robert Palmer
IPC分类号： G06F9/44
CPC分类号： G06F8/433 , G06F8/456 , G06F11/3608
摘要： Described techniques and tools help model checking scale to large programs while reducing missed errors. In particular, described techniques and tools help reduce the state space of concurrent programs without depending on cycle detection and without scheduling execution of postponed threads at all cycles. For example, described techniques and tools use a type of partial-order reduction called transaction-based reduction to reduce program state space. Analysis is performed at commit points to determine whether to schedule delayed threads.
摘要翻译：描述的技术和工具可帮助模型检查大型程序的规模，同时减少错误的错误。特别地，所描述的技术和工具有助于减少并发程序的状态空间，而不依赖于周期检测，并且不调度在所有周期执行延迟的线程。例如，所描述的技术和工具使用一种称为基于事务的减少的部分顺序减少来减少程序状态空间。分析在提交点执行，以确定是否计划延迟的线程。

12. 发明申请

US20060130010A1 Model checking with bounded context switches 失效
标题翻译：使用有界的上下文切换进行模型检查
公开(公告)号：US20060130010A1
公开(公告)日：2006-06-15
申请号：US11009752
申请日：2004-12-10
申请人： Niels Rehof , Shaz Qadeer
发明人： Niels Rehof , Shaz Qadeer
IPC分类号： G06F9/45
CPC分类号： G06F11/3608
摘要： Validity of one or more assertions for any concurrent execution of a plurality of software instructions with at most k−1 context switches can be determined. Validity checking can account for execution of the software instructions in an unbounded stack depth scenario. A finite data domain representation can be used. The software instructions can be represented by a pushdown system. Validity checking can account for thread creation during execution of the plurality of software instructions.
摘要翻译：可以确定用于任何并发执行多达k-1个上下文切换的多个软件指令的一个或多个断言的有效性。有效性检查可以解释在无限堆栈深度场景中执行软件指令。可以使用有限数据域表示。软件指令可以由下推系统表示。有效性检查可以解释执行多个软件指令期间的线程创建。

13. 发明申请

US20130239120A1 CONCURRENT ASSERTION 有权
标题翻译：当前评估
公开(公告)号：US20130239120A1
公开(公告)日：2013-09-12
申请号：US13415854
申请日：2012-03-09
申请人： Jacob Samuels Burnim , Madanlal Musuvathi , Shaz Qadeer
发明人： Jacob Samuels Burnim , Madanlal Musuvathi , Shaz Qadeer
IPC分类号： G06F9/46
CPC分类号： G06F11/3604 , G06F9/4881 , G06F11/366
摘要： A concurrency assertions system disclosed herein provides for atomic evaluation of an assertion expression by locking an assertion lock upon initiating an assertion and thereby protecting the assertion evaluation from concurrent modifications to the variables in the assertion expressions. When a violation of an assertion is detected, the concurrency assertions system ensures that the exception statistics at the time of the assertion violation represents a program state where the assertion is violated, thus improving analysis of assertion violations. Furthermore, the concurrency assertions system continuously evaluates an expression for an assertion for a time period while other threads in the program are being executed.
摘要翻译：本文公开的并发断言系统提供了通过在发起断言时锁定断言锁定从而保护断言评估免于对断言表达式中的变量的并发修改来对断言表达式进行原子评估。当检测到断言的违反时，并发断言系统确保在断言违规时的异常统计信息表示违反断言的程序状态，从而改善断言违规的分析。此外，并发断言系统在执行程序中的其他线程的同时持续评估断言的表达式。

14. 发明申请

US20100169868A1 Unifying Type Checking and Property Checking for Low Level Programs 有权
标题翻译：统一类型检查和低级程序的属性检查
公开(公告)号：US20100169868A1
公开(公告)日：2010-07-01
申请号：US12347398
申请日：2008-12-31
申请人： Jeremy P. Condit , Shaz Qadeer , Shuvendu K. Lahiri
发明人： Jeremy P. Condit , Shaz Qadeer , Shuvendu K. Lahiri
IPC分类号： G06F9/45 , G06F9/44
CPC分类号： G06F8/437 , G06F8/40 , G06F11/3608
摘要： This document describes a unified type checker and property checker for a low level program's heap and its types. The type checker can use the full power of the property checker to express and verify subtle, program specific type and memory safety invariants well beyond what the native low level program system can check. Meanwhile, the property checker can rely on the type checker to provide structure and disambiguation for the program's heap, enabling more concise and more powerful type-based specifications. This approach makes use of a fully automated Satisfiability Modulo Theories (SMT) solver and a decision procedure for checking type safety, which means that the programmer's only duty is to provide high-level type and property annotations as part of the original program's source.
摘要翻译：本文档描述了低级程序堆及其类型的统一类型检查器和属性检查器。类型检查器可以使用属性检查器的全部功能来表达和验证微妙的程序特定类型和内存安全不变量，远远超出了本机低级程序系统可以检查的内容。同时，属性检查器可以依靠类型检查器为程序的堆提供结构和消歧，从而实现更简洁和更强大的基于类型的规范。这种方法利用完全自动化的满意度模数理论（SMT）求解器和检查类型安全性的决策程序，这意味着程序员唯一的职责是提供高级类型和属性注释作为原始程序源的一部分。

15. 发明授权

US07316005B2 Data race detection using sequential program analysis 有权
标题翻译：数据竞赛检测采用顺序程序分析
公开(公告)号：US07316005B2
公开(公告)日：2008-01-01
申请号：US10765717
申请日：2004-01-26
申请人： Shaz Qadeer , Dinghao Wu
发明人： Shaz Qadeer , Dinghao Wu
IPC分类号： G06F9/44
CPC分类号： G06F11/3608
摘要： A concurrent program is analyzed for the presence of data races by the creation of a sequential program from the concurrent program. The sequential program contains assertions which can be verified by a sequential program analysis tool, and which, when violated, indicate the presence of a data race. The sequential program emulates multiple executions of the concurrent program by nondeterministically scheduling asynchronous threads of the concurrent program on a single runtime stack and nondeterministically removing the currently-executing thread from the stack before instructions of the program. Checking functions are used to provide assertions for data races, along with a global access variable, which indicates if a variable being analyzed for data races is currently being accessed by any threads.
摘要翻译：通过从并发程序创建顺序程序，分析并发程序是否存在数据竞赛。顺序程序包含断言，可以通过顺序程序分析工具进行验证，如果违规则指示数据竞赛的存在。顺序程序通过在单个运行时堆栈上非确定性地调度并发程序的异步线程来模拟并发程序的多次执行，并且在程序的指令之前非确定性地从堆栈中去除当前执行的线程。检查功能用于为数据竞赛提供断言，以及全局访问变量，指示当前正在由任何线程访问正在分析数据竞争的变量。

16. 发明授权

US06892319B2 Method for verifying abstract memory models of shared memory multiprocessors 有权
标题翻译：用于验证共享存储器多处理器的抽象存储器模型的方法
公开(公告)号：US06892319B2
公开(公告)日：2005-05-10
申请号：US09949324
申请日：2001-09-07
申请人： Shaz Qadeer
发明人： Shaz Qadeer
IPC分类号： G06F11/28 , G06F12/08 , G06F11/00
CPC分类号： G06F11/28 , G06F12/0815
摘要： A method of verifying a protocol for a shared-memory multiprocessor system for sequential consistency. In the system there are n processors and m memory locations that are shared by the processors. A protocol automaton, such as a cache coherence protocol automaton, is developed. The protocol automaton and a plurality of checker automata are provided to a model checker which exhaustively searches the state space of the protocol automaton. During the search, the plurality of checker automata check for the presence of cycles in a graph that is the union of the total orders of the processor references and the partial orders at each memory location. If the plurality of checker automata detect the presence of a cycle, then the protocol does not meet the sequential consistency requirement.
摘要翻译：一种验证用于顺序一致性的共享存储器多处理器系统的协议的方法。在系统中，处理器共有n个处理器和m个存储器位置。开发了协议自动机，如缓存一致性协议自动机。协议自动机和多个检验自动机被提供给一个模拟检查器，该检查器彻底地搜索协议自动机的状态空间。在搜索期间，多个检查器自动机检查在图中是否存在循环，其是处理器参考的总顺序和每个存储器位置处的部分顺序的并集。如果多个检验自动机检测到循环的存在，则该协议不符合顺序一致性要求。

17. 发明授权

US09329877B2 Static verification of parallel program code 有权
标题翻译：并行程序代码的静态验证
公开(公告)号：US09329877B2
公开(公告)日：2016-05-03
申请号：US13423255
申请日：2012-03-18
申请人： Alastair Francis Donaldson , Shaz Qadeer
发明人： Alastair Francis Donaldson , Shaz Qadeer
IPC分类号： G06F9/44 , G06F9/445
CPC分类号： G06F9/44589
摘要： A symbolic encoding of predicated execution for static verification, based on a plurality of data parallel program instructions, is obtained. A result of static verification of one or more attributes associated with the plurality of data parallel program instructions is obtained, based on the symbolic encoding.
摘要翻译：获得基于多个数据并行程序指令的用于静态验证的预定执行的符号编码。基于符号编码获得与多个数据并行程序指令相关联的一个或多个属性的静态验证的结果。

18. 发明授权

US09063778B2 Fair stateless model checking 有权
标题翻译：公平的无状态模型检查
公开(公告)号：US09063778B2
公开(公告)日：2015-06-23
申请号：US11971656
申请日：2008-01-09
申请人： Madanlal Musuvathi , Shaz Qadeer
发明人： Madanlal Musuvathi , Shaz Qadeer
IPC分类号： G06F9/46 , G06F9/48
CPC分类号： G06F9/4881 , G06F2209/484
摘要： 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.
摘要翻译：公开了提供公平无状态模型检查器的技术。在某些方面，生成一个调度表来为多线程程序的线程分配资源，代替具有为线程分配资源的操作系统。生成的时间表是公平和详尽的。在一个实施例中，当确定不同的线程不进行时，可以实现优先级图表来重新调度线程。然后，模型检查器可以在程序中实现所生成的计划之一，以便确定在程序的特定执行期间是否发生错误或活锁。模型检查器的输出可以有助于识别错误和/或活动锁定，或者将程序认证为正确操作。

19. 发明授权

US08813043B2 Unifying type checking and property checking for low level programs 有权
标题翻译：对低级程序进行统一的类型检查和属性检查
公开(公告)号：US08813043B2
公开(公告)日：2014-08-19
申请号：US12347398
申请日：2008-12-31
申请人： Jeremy P. Condit , Shaz Qadeer , Shuvendu K. Lahiri
发明人： Jeremy P. Condit , Shaz Qadeer , Shuvendu K. Lahiri
IPC分类号： G06F9/44 , G06F9/45 , G06F11/36
CPC分类号： G06F8/437 , G06F8/40 , G06F11/3608
摘要： This document describes a unified type checker and property checker for a low level program's heap and its types. The type checker can use the full power of the property checker to express and verify subtle, program specific type and memory safety invariants well beyond what the native low level program system can check. Meanwhile, the property checker can rely on the type checker to provide structure and disambiguation for the program's heap, enabling more concise and more powerful type-based specifications. This approach makes use of a fully automated Satisfiability Modulo Theories (SMT) solver and a decision procedure for checking type safety, which means that the programmer's only duty is to provide high-level type and property annotations as part of the original program's source.
摘要翻译：本文档描述了低级程序堆及其类型的统一类型检查器和属性检查器。类型检查器可以使用属性检查器的全部功能来表达和验证微妙的程序特定类型和内存安全不变量，远远超出了本机低级程序系统可以检查的内容。同时，属性检查器可以依靠类型检查器为程序的堆提供结构和消歧，从而实现更简洁和更强大的基于类型的规范。这种方法利用完全自动化的满意度模数理论（SMT）求解器和检查类型安全性的决策程序，这意味着程序员唯一的职责是提供高级类型和属性注释作为原始程序源的一部分。

20. 发明授权

US07752605B2 Precise data-race detection using locksets 失效
标题翻译：使用锁具进行精确的数据竞赛检测
公开(公告)号：US07752605B2
公开(公告)日：2010-07-06
申请号：US11403414
申请日：2006-04-12
申请人： Shaz Qadeer , Tayfun Elmas
发明人： Shaz Qadeer , Tayfun Elmas
IPC分类号： G06F9/44
CPC分类号： G06F11/3632
摘要： A data race detection system is described which precisely identifies data races in concurrent programs. The system and techniques described utilize locksets to maintain information while searching through executions of a concurrent program. The locksets are updated according to program statements in the concurrent program. The dynamic updating of the locksets, combined with a less conservative approach then used in existing lockset data race detection techniques, allows the technique to be precise; that is, the technique does not report false positives when searching a program.
摘要翻译：描述了数据竞争检测系统，其精确地识别并发程序中的数据竞赛。所描述的系统和技术利用锁定装置来维护信息，同时在执行并行程序的同时进行搜索。根据并发程序中的程序语句更新锁定。锁定器的动态更新与现有锁定数据种族检测技术中使用的较不保守的方法相结合，使得该技术是精确的; 也就是说，在搜索程序时，该技术不会报告错误的肯定。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式