مدلهای همزمانی و حسابهای فرایند
مدلهای همزمانی و حسابهای فرایند، توصیفهای رسمی از چگونگی اجرای فرایندهای مستقل، ارتباط و همگامسازی آنها ارائه میدهند.
Definition
حساب فرایند (process calculus) یک جبر رسمی برای توصیف سیستمهای همزمان به عنوان فرایندهای ارتباطی است، با عملگرهایی برای ترکیب موازی، ارتباط و انتخاب، و همارزیهایی که تعیین میکنند چه زمانی دو فرایند رفتار یکسانی دارند.
Scope
این موضوع مدلهای جبری محاسبات همزمان را پوشش میدهد: CSP هوآر و CCS میلنر، پی-حساب (pi-calculus) برای فرایندهای متحرک که توپولوژی ارتباطی آنها تغییر میکند، و مدل عامل (actor model) پیامرسانی ناهمزمان. همچنین به اصول اولیه ارتباط و همگامسازی، همارزیهای رفتاری مانند همشبیهسازی (bisimulation)، و تفاوت بین همزمانی حافظه مشترک و پیامرسانی میپردازد.
Core questions
- چگونه میتوان فرایندهای همزمان ارتباطی را به صورت جبری توصیف کرد؟
- چه زمانی دو فرایند همزمان از نظر رفتاری همارز هستند؟
- پیامرسانی در مقایسه با همزمانی حافظه مشترک چگونه است؟
- ساختارهای ارتباطی پویا چگونه مدلسازی میشوند، مانند پی-حساب؟
Key theories
- فرایندهای ترتیبی ارتباطی (CSP)
- CSP هوآر همزمانی را از طریق فرایندهایی مدلسازی میکند که بر رویدادهای ارتباطی مشترک همگامسازی میشوند و مبنایی برای زبانهای پیامرسانی و نظریهای برای پالایش فرایند فراهم میکند.
- CCS و همشبیهسازی (bisimulation)
- حساب سیستمهای ارتباطی میلنر (CCS) جبری از فرایندها را با مفهومی دقیق از همارزی رفتاری، یعنی همشبیهسازی، برای استدلال در مورد زمان قابل تعویض بودن فرایندها ارائه میدهد.
- پی-حساب (The pi-calculus)
- میلنر، پارو و واکر حسابهای فرایند را به سمت قابلیت تحرک گسترش دادند و اجازه دادند که خود کانالهای ارتباطی به عنوان پیام منتقل شوند تا ساختار اتصال به صورت پویا تکامل یابد.
Clinical relevance
حسابهای فرایند و مدل عامل، زیربنای طراحی زبانها و چارچوبهای همزمان و توزیعشده مبتنی بر پیامرسانی هستند و ابزارهای رسمی برای مشخص کردن و تأیید پروتکلها فراهم میکنند. همشبیهسازی (bisimulation) و پالایش (refinement) معیارهای دقیقی برای رفتار همزمان صحیح ارائه میدهند.
History
نظریه همزمانی در اواخر دهه 1970 با CSP هوآر و CCS میلنر به بلوغ رسید، در حالی که مدل عامل (actor model) هیویت (1973) یک جایگزین پیامرسانی ناهمزمان ارائه داد. پی-حساب (pi-calculus) در سال 1992 قابلیت تحرک فرایند را به تصویر کشید. این حسابها بر زبانهای پیامرسانی و کتابخانههای همزمانی تأثیر گذاشتند و همچنان مبنایی برای تأیید پروتکلها هستند.
Debates
- حافظه مشترک در مقابل پیامرسانی
- یک سوال اساسی در طراحی این است که آیا همزمانی باید حول حالت مشترک قابل تغییر با همگامسازی سازماندهی شود یا حول فرایندهای ایزوله که پیامها را مبادله میکنند، با حسابهای فرایند و مدل عامل که از دومی حمایت میکنند.
Key figures
- C. A. R. Hoare
- Robin Milner
- Carl Hewitt
- Joachim Parrow
- David Walker
Related topics
Seminal works
- hoare1978
- milner1989
- milner1992
- hewitt1973
Frequently asked questions
- همشبیهسازی (bisimulation) چیست؟
- همشبیهسازی یک همارزی در فرایندها است که زمانی برقرار است که هر یک بتواند گامهای قابل مشاهده دیگری را به طور نامحدود مطابقت دهد و ایده اینکه دو فرایند همزمان رفتار یکسانی از خود نشان میدهند را رسمی میکند.
- پی-حساب (pi-calculus) چه چیزی را نسبت به حسابهای قبلی اضافه میکند؟
- پی-حساب قابلیت تحرک را با اجازه دادن به ارسال کانالهای ارتباطی به عنوان پیام مدلسازی میکند، بنابراین توپولوژی اینکه چه کسی میتواند با چه کسی صحبت کند، میتواند در طول اجرا تغییر کند و سیستمهای پویا و قابل پیکربندی مجدد را به تصویر میکشد.