TAILIEUCHUNG - CONCUR 2004 – Concurrency Theory- P2

CONCUR 2004 – Concurrency Theory- P2: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | A Semantics for Concurrent Separation Logic Stephen Brookes Carnegie Mellon University Department of Computer Science Abstract. We present a denotational semantics based on action traces for parallel programs which share mutable data and synchronize using resources and conditional critical regions. We introduce a resource-sensitive logic for partial correctness adapting separation logic to the concurrent setting as proposed by O Hearn. The logic allows program proofs in which ownership of a piece of state is deemed to transfer dynamically between processes and resources. We prove soundness of this logic using a novel local interpretation of traces and we show that every provable program is race-free. 1 Introduction Parallel programs involve the concurrent execution of processes which share state and are intended to cooperate interactively. It is notoriously difficult to ensure absence of runtime errors such as races in which one process changes a piece of state being used by another process and dangling pointers which may occur if two processes attempt simultaneously to deallocate the same storage. Such phenomena can cause unpredictable or irreproducible behavior. Rather than relying on assumptions about the granularity of hardware primitives it is preferable to use program design rules and proof techniques that guarantee error-freedom. The classic example is the syntax-directed logic for partial correctness properties of pointer-free parallel programs introduced by Owicki and Gries 15 building on prior work of Hoare 7 . This approach focusses on critical variables the identifiers concurrently written by one process and read or written by another. The programmer must partition the critical variables among named resources and each occurrence of a critical variable must be inside a region naming the relevant resource. Assuming that resource management is implemented by a suitable synchronization primitive such as semaphores 6 1 the design rules guarantee mutually .

• Phần cứng
• kiến trúc máy tính
• bo mạch chủ
• giáo trình phần cứng máy tính
• vận hành của BIOS
• Cạc mạng
• lắp ráp máy tính
• Trắc nghiệm kiến trúc máy tính
• Bài tập kiến trúc máy tính
• Ôn tập kiến trúc máy tính
• Câu hỏi kiến trúc máy tính
• Tài liệu kiến trúc máy tính
• Đại cương kiến trúc máy tính
• Tổng quan kiến trúc máy tính
• Lịch sử kiến trúc máy tính
• Bài giảng kiến trúc máy tính
• Hệ thống máy tính
• cấu trúc máy tính
• ôn thi môn kiến trúc máy tính
• đề cương kiến trúc máy tính
• tài liệu về kiến trúc máy tính
• tìa liệu về kiến trúc máy tính
• Sách kiến trúc máy tính
• Cấu tạo máy tính
• Đề cương ôn tập kiến trúc máy tính
• Câu hỏi trắc nghiệm kiến trúc máy tính
• Cấu tạo kiến trúc máy tính
• Giáo trình kiến trúc máy tính
• Cấu trúc phần cứng của máy tính
• Kiến trúc Von Neumann
• Cấu trúc của một máy tính hiện đại
• Bộ vi xử lý trung tâm máy tính
• Bộ nguồn máy tính
• Hệ thống kiến trúc máy tính
• Tìm hiểu kiến trúc máy tính
• Lý thuyết kiến trúc máy tính
• Nguyên lý kiến trúc máy tính