tgoop.com/pythonwithmedev/411
Last Update:
"Non-determinism، Nondeterminism، Non Determinism، or Nondet"
بخش اول
—————————————————————
میتونم بگم دو به شکام که جذابترین کانسپتی که در تمام مباحث TCS تا به حال باهاش مواجه بودم، Fairness هستش یا Non-determinism. یکی از نقطه اشتراکات هر دو مبحث برام اینه که از نظر فسلفی آیا حقیقت وجودی دارند و یا صرفا برای پر کردن خلاای در علم توسط بشر ابداع شدند که را حل منطقی و درستی براش وجود نداشته. یه نکته جالب دیگهای که میتونم در موردش بگم اینه که از نظر من Fairness و Non-determinism به شکل Natural در مسائل وجود ندارند ولی از یک جایی که انگار فرای اختیارات ماست به مسائل Enforce میشن. این نوشته قصد داره که به مفهوم دوم بپردازه منتهی قبلش جا داره این هشدار رو بدم که Non-determinism گاهی اوقات از نظر شهودی یک پدیدهی Stochastic تفسیر میشه که خیلی درست نیست برای همین سعی میکنم از ادبیات درستی استفاده کنم در ادامه.
خودم به شخصه اولین جایی که در دوران تحصیل چه به شکل فرمال و چه غیر فرمال با مفهومی به نام Non-determinism مواجه شدم توی درس آتوماتا تئوری بود. مدلهای محاسباتیای که مبتنی بر مفهوم state و transition هستند و براساس همین state و transition هم مفهوم عدم قطعیت به شکل فرمال تعریف میشه. اولین شوک و نکتهی جالبی که باهاش مواجه شدم اینه که مدلهایی که non-determinism دارن، همیشه براشون یک مدل محاسباتی Deterministic وجود نداره و برخی مواقع افزودن Non-determinism به مدل محاسباتی منجر به افزایش Expressiveness این مدل میشه. مثل Büchi Automata.
دومین جایی که با این کانسپت به طور جدی مواجه شدم توی فرمال متد بود. زبانها و مدلهای صوری که برای جنبههای مختلف یک محاسبه ایجاب میشدن هم Non-determinism داشتن. به طور مثال زبان Guarded Command Language آقای دایکسترا که به نظرم پایهگزار زبانهای برنامهنویسی Imperative بود non-determinism داشت. به طوری که مثلا شما میتونید برنامهای بنویسید بدین صورت :
if
[] a > 0 ——> b = false
[] a > 3 ——> b = true
fi
طبق semantics این زبان شما در این دستور if اگر مقدار a از 3 بزرگتر باشه، Guard هر دو command ارضا میشه و یکی از دو دستور به شکل غیرقطعی اجرا میشه.
سومین جایی که این کانسپت رو دیدم توی Concurrency Theory بود. زمانی که ما چند instance از یک مدل محاسباتی یا برنامههایی از یک زبان فرمال داریم مثل P1,P2, ...., Pn که با استفاده از اپراتور parallel composition یک برنامهی جدید رو میسازن :
p1
و طبق سمنتیکس این اپراتور، دستورات اتومیک هر Pi با رعایت program order خودش میتونه با هر ترتیب ممکنی با دستورات اتومیک باقی Pj ها interleave بشه. مثلا اگر شما دو تا برنامه داشته باشی مثل :
p1 : R(x) W(x)
p2 : R(y) W(y)
اون وقت برنامهی P1 P2 میتونه در هر اجرا یک trace اجرایی متفاوتی داشته باشه مثل :
R(x) W(x) R(y) W(y)
R(x) R(y) W(x) W(y)
R(x) R(y) W(y) W(x)
R(y) W(y) R(x) W(x)
R(y) R(x) W(y) W(x)
R(y) R(x) W(x) W(y)
اصطلاحا به این ویژگی میگن Scheduling non-determinism که بزرگترین معضلای هست که در verify کردن برنامههای parallel و distributed باهاش دست و پنجه نرم میکنیم.
چهارمین جایی که با این مفهوم مواجه شدم در Verification بود. زمانی که داشتم JMC رو میساختم به این مسئله برخورد کردیم که همیشه در برنامههای concurrent تنها منبع عدم قطعیت Scheduling nondeterminism نیست. به برنامهی زیر توجه کنید :
void foo (int x) {
if( x % 3 == 2) {
// Bug
} else {
print("All is good!");
}
}
در این برنامه یک عدم قطعیتی وجود داره که ما اسمش رو گذاشتیم Data nondeterminism و شد موضوع مقالهای که چند روز پیش سابمیت کردیم. در این برنامه با توجه به مقدار آرگومان x، رفتار برنامه تغییر میکنه. ما اومدم چهار لول data nondeterminism تعریف کریم و براش یک سمنتیکس dpor-based ارائه دادیم. ما نشون دادیم که data non-determinism یک مفهوم orthogonal با scheduling non-determinism نیست و یک الگوریتم مدل چکینگ ارائه دادیم برای برنامههایی مالتی تردی که data non-determinism دارند، مثل concurrent data structures ها، که sound و complete و optimal هستش. علاوه بر اینا و شاید مهم تر از اینا، ما یک Reduction از Scheduling nondeterminism به Data nondeterminism ارائه کردیم که باعث کاهش چشمگیر فضای حالت برنامه میشه. حالا جزئیاتش باشه ایشالا اگر چاپ شد توی کانال بهش میپردازم.
اما ما اولین نفرهایی نبودیم که اومدم کانسپت non-determinism رو سطح بندی کردیم. در ادامه میخوام به چندتا مقاله که به شدت خوب و روون نوشته شدن رو بهتون معرفی کنم که بحث اصلیشون کلاسهبندی Nondeterminism هستش.
BY 🧑💻Cyber.vision🧑💻
Share with your friend now:
tgoop.com/pythonwithmedev/411