A complex object is an abstraction and description of a complex entity of the real world. Many applications in such domains as CIMS, CAD and OA define and manipulate a complex object as a single unit. In this paper, a...A complex object is an abstraction and description of a complex entity of the real world. Many applications in such domains as CIMS, CAD and OA define and manipulate a complex object as a single unit. In this paper, a definition of the model of complex objects is given, and the concurrency control mechanism of complex objects in WHYMX object-oriented database system is described.展开更多
Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for softwar...Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for software transactional memory(STM)and in anonymous and fault-tolerant distributed computing.However,existing work can only verify obstruction-freedom of specific data structures(e.g.,STM and list-based algorithms).In this paper,to fill this gap,we propose a program logic that can formally verify obstruction-freedom of practical implementations,as well as verify linearizability,a safety property,at the same time.We also propose informal principles to extend a logic for verifying linearizability to verifying obstruction-freedom.With this approach,the existing proof for linearizability can be reused directly to construct the proof for both linearizability and obstruction-freedom.Finally,we have successfully applied our logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.展开更多
Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementat...Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.展开更多
基金This research is supported by National Natural Science Foundation of China
文摘A complex object is an abstraction and description of a complex entity of the real world. Many applications in such domains as CIMS, CAD and OA define and manipulate a complex object as a single unit. In this paper, a definition of the model of complex objects is given, and the concurrency control mechanism of complex objects in WHYMX object-oriented database system is described.
基金the National Natural Science Foundation of China(Grant No.61632005)。
文摘Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for software transactional memory(STM)and in anonymous and fault-tolerant distributed computing.However,existing work can only verify obstruction-freedom of specific data structures(e.g.,STM and list-based algorithms).In this paper,to fill this gap,we propose a program logic that can formally verify obstruction-freedom of practical implementations,as well as verify linearizability,a safety property,at the same time.We also propose informal principles to extend a logic for verifying linearizability to verifying obstruction-freedom.With this approach,the existing proof for linearizability can be reused directly to construct the proof for both linearizability and obstruction-freedom.Finally,we have successfully applied our logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.
基金supported by the National Natural Science Foundation of China under Grant No.61632005。
文摘Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.
