کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | ترجمه فارسی | نسخه تمام متن |
---|---|---|---|---|---|
4951397 | 1441449 | 2017 | 17 صفحه PDF | سفارش دهید | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Formalization of Habanero phasers using Coq
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
سفارش ترجمه تخصصی
با تضمین قیمت و کیفیت
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
Phasers pose an interesting synchronization mechanism that generalizes many collective synchronization patterns seen in parallel programming languages, including barriers, clocks, and point-to-point synchronization using latches or semaphores. This work characterizes scheduling constraints on phaser operations, by relating the execution state of two tasks that operate on the same phaser. We propose a formalization of Habanero phasers, May-Happen-In-Parallel, and Happens-Before relations for phaser operations, and show that these relations conform with the semantics. Our formalization and proofs are fully mechanized using the Coq proof assistant, and are available online.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 90, August 2017, Pages 50-60
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 90, August 2017, Pages 50-60
نویسندگان
Tiago Cogumbreiro, Jun Shirako, Vivek Sarkar,
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
سفارش ترجمه تخصصی
با تضمین قیمت و کیفیت