کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4950628 | 1440714 | 2017 | 18 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Lost in abstraction: Monotonicity in multi-threaded programs
ترجمه فارسی عنوان
از دست رفته در انتزاع: تک تنه در برنامه های چند رشته
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
نرم افزار چند رشته ای تأیید پارامتریک یکنواختی، انتزاع پیش بینی،
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
Monotonicity in concurrent systems stipulates that, in any global state, system actions remain executable when new processes are added to the state. This concept is both natural and useful: if every thread's memory is finite, monotonicity often guarantees the decidability of safety properties even when the number of running threads is unknown. In this paper, we show that finite-data thread abstractions for model checking can be at odds with monotonicity: predicate-abstracting monotone software can result in non-monotone Boolean programs - the monotonicity is lost in the abstraction. As a result, pertinent well-established safety checking algorithms for infinite-state systems become inapplicable. We demonstrate how monotonicity in the abstraction can be restored, without affecting safety properties. This improves earlier approaches of enforcing monotonicity via overapproximations. We implemented our solution in the unbounded-thread model checker monabs and applied it to numerous concurrent programs and algorithms, whose predicate abstractions are often fundamentally beyond existing tools.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 252, February 2017, Pages 30-47
Journal: Information and Computation - Volume 252, February 2017, Pages 30-47
نویسندگان
Alexander Kaiser, Daniel Kroening, Thomas Wahl,