Đang chuẩn bị liên kết để tải về tài liệu:
CONCUR 2004 – Concurrency Theory- P2

Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ

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 .

TAILIEUCHUNG - Chia sẻ tài liệu không giới hạn
Địa chỉ : 444 Hoang Hoa Tham, Hanoi, Viet Nam
Website : tailieuchung.com
Email : tailieuchung20@gmail.com
Tailieuchung.com là thư viện tài liệu trực tuyến, nơi chia sẽ trao đổi hàng triệu tài liệu như luận văn đồ án, sách, giáo trình, đề thi.
Chúng tôi không chịu trách nhiệm liên quan đến các vấn đề bản quyền nội dung tài liệu được thành viên tự nguyện đăng tải lên, nếu phát hiện thấy tài liệu xấu hoặc tài liệu có bản quyền xin hãy email cho chúng tôi.
Đã phát hiện trình chặn quảng cáo AdBlock
Trang web này phụ thuộc vào doanh thu từ số lần hiển thị quảng cáo để tồn tại. Vui lòng tắt trình chặn quảng cáo của bạn hoặc tạm dừng tính năng chặn quảng cáo cho trang web này.