کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4951421 | 1441450 | 2017 | 26 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Revisiting concurrent separation logic
ترجمه فارسی عنوان
بازبینی منطق جداسازی همزمان
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
منطق جداسازی همزمان، معانی عملیاتی سازمانی، صدا ثابت،
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
We present a new soundness proof of Concurrent Separation Logic (CSL) based on a structural operational semantics (SOS). We build on two previous proofs and develop new auxiliary notions to achieve the goal. One uses a denotational semantics (based on traces). The other is based on SOS, but was obtained only for a fragment of the logic - the Disjoint CSL - which disallows modifying shared variables between concurrent threads. In this work, we lift such a restriction, proving the soundness of full CSL with respect to a SOS. Thus contributing to the development of tools able of ensuring the correctness of realistic concurrent programs. Moreover, given that we used SOS, such tools can be well-integrated in programming environments and even incorporated in compilers.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 89, June 2017, Pages 41-66
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 89, June 2017, Pages 41-66
نویسندگان
Pedro Soares, António Ravara, Simão Melo de Sousa,