"Just run the goddamn code" - P.1
——————————————————

خب امروز آخر جلسه یه بحثی شد در مورد مدل چکینگ و به طور خاص Stateless Model Checking. به چند تا ابزار خاص اشاره کردیم که کارشون تست کردن برنامه‌های concurrent و distributed ای هستش که با یک زبان برنامه‌نویسی نوشته میشن. این ابزارها معماری‌شون به طور abstract بدین صورته که از ۳ جزء خیلی مهم تشکیل میشن :

1. Instrumentation :

پروسه‌ی test با این فاز شروع میشه. توی این قسمت برنامه از ورودی خونده میشه و روی سینتکسش تغییراتی صورت میگیره و چیزهایی اضافه میشه. این تغییرات در بهترین حالت باید روی کد میانی این زبان‌ها اجرا بشن. یعنی بعد از کامپایل شدن. به‌طور مثال در زبان‌های مبتنی بر JVM این تغییرات باید روی bytecode حاصل از compile صورت بگیره. اما دقیقا چه چیزهایی دست‌خوش تغییرات میشن؟ اولین چیز اینه که ما باید تمام عملیات‌های مربوط به concurrency رو تشخیص بدیم. برای مثال وقتی که یک thread یا process میخواد مقداری رو از روی یک shared variable بخونه و یا بنویسه ( عملیات‌های read و write) یا زمانی که یک ترد یا پراسس قراره ساخته بشه و استارت بشه (create , start) زمانی که یک ترد یا پراسس میخواید terminate بشه یا join بشه (join و terminate). این‌ها عملیات‌های پایه هستند و به محض شناسایی این دستورات در بایت‌کد، میایم و یک breakpoint قبل و بعد صدا شدن این دستورات قرار میدیم. این breakpoint ها میتونه صدا زدن یک تابع باشن که خودمون نوشتیم ( توی بخش دوم بیشتر توضیح میدم). علاوه بر عملیات‌های پایه باید توی کد بریم و ببینیم از چه کتابخونه‌ها و api هایی مربوط به concurrency استفاده شده. به طور مثال شما توی جاوا میتونید برای انجام عملیات‌های atomic از پکیج atomic استفاده کنید. این پکیج اجازه میده شما متغیرهایی رو از تایپ‌های atomicInteger و atomicBoolean و ... تعریف کنید و عملیات‌های اتومیک مثل compare-and-set روشون انجام بدید. کاری که باید انجام بدید اینه که تمام این api ها و کتاب‌خونه ها رو بریم کدشون رو کپی کنیم و توی یه پیکیج جدید paste کنیم و اون breakpoint ها رو جاهای درستی قرار بدیم ( به عبارت دیگه این مرحله در سطح زبان انجام میشه نه بایت کد). در ادامه هر جای که یک ترد یا پراسس از اون کتابخونه یا api استفاده کرده، آدرس پکیجش رو با اونی که خودمون نوشتیم عوض کنیم.

2. Runtime :

حالا کاری که باید انجام بدیم نوشتن یک runtime بسیار بسیار سبک و جمع جوره. چرا ما به یک runtime نیاز داریم؟ چون قراره که مدیریت scheduling تردها و پراسس‌ها رو دست بگیریم. یعنی قراره که runtime ما قبل از تست برنامه‌ی کاربر لود بشه و کنترل مدیریت تردها و پراسس‌های برنامه‌ی کاربر رو دست بگیره. اون توابعی هم که توی قسمت قبل تحت عنوان breakpoint اضافه کردیم، در حقیقت ارجاع دادن به همین runtime هست. به طور مثال یک ترد حین اجرا قراره عملیات write انجام بده. قبل از انجام عملیات، این قضیه رو به runtime اطلاع میده و wait میکنه. بعد scheduler بیدار میشه و تصمیم میگیره که آیا به اون ترد اجازه انجام write رو بده یا یک ترد دیگه رو resume کنه (توضیحات بیشتر در قسمت سوم). با plug and play کردن این runtime با کد instrument شده‌ی کاربر، ابزار ما میاد و برنامه‌ی کاربر رو با اجرا کردن برنامه تست میکنه. چیزی که توی runtime نیاز داریم داشته باشیم یک ترد scheduler برای مدیریت ترد‌هاست و علاوه بر اون نیازه که یک state بسیار کوچک و محدود از تردها نگه داریم. مثلا اینکه چندتا ترد توی برنامه در حال اجراست. یا تردها هر کدوم توی چه وضعیتی هستند. یا اینکه هر ترد چه منابعی رو (مثل lock) در اختیار داره و چه منابعی رو درخواست داده که بگیره. نگه داری این اطلاعات برای انجام scheduling لازمه و حتی کمک میکنه که deadlock و چیزهای شبیه به این رو هم کشف کنیم. توجه کنید، درسته که برنامه‌ی کاربر مالتی‌ترد هست و تردها در عمل به شکل همزمان با هم اجرا میشن، اما runtime ما تضمین میکنه که در هر لحظه فقط یک ترد از برنامه‌ی کاربر در حال اجراست و به نوعی میایم اجرای برنامه رو serialize میکنیم. این امر به ما کمک میکنه که بتونیم درستی ابزار خودمون رو بررسی کنیم و همه چیز تحت کنترل‌مون باشه.