"Software Verification is Our Business"
————————————————————

به‌طور خلاصه شما برنامه‌ مد نظرتون رو به عنوان ورودی میدید به JMC و نوع strategy ای که قرار هست JMC به واسطه‌ی اون برنامه تون رو وریفای کنه رو مشخص میکنید. ما توی JMC یک runtime environment و یک Scheduler نوشتیم که میاد و روی JVM سوار میشه و کنترل Schedule کردن Thread های برنامه‌ی شما رو بدست میگیره. حالا کاری که Scheduler میخواد انجام بده اینه که Thread های شما رو طوری توی هم Interleave کنه که برنامه‌ی شما به باگ بخوره. به این روش اصطلاحا میگن Stateless Model Checking که بعدا توی کانال بیشتر در موردش توضیح میدم و اگر اطلاعات بیشتری خواستید این مقاله رو بخونید.

حالا سوالی که پیش میاد اینه که Scheduler چطور باید Thread ها رو Schedule کنه که به باگ بخوریم و اصلا باگ قراره چی باشه. در حال حاضر JMC دو نوع باگ رو میتونه توی برنامه‌ی شما پیدا کنه. اولیش اینه که Thread های شما برای Sync شدن میتونن از Monitor استفاده کنند، از اونجایی که Monitor ها بین Thread ها به اشتراک گذاشته شدن، امکان ایجاد ددلاک هست. JMC میتونه وجود هر گونه Deadlock احتمالی در استفاده از Monitor توسط Thread های توی کدتون رو پیدا کنه. دومین باگ Assertion Violation هست. شما توی کدتون هر جایی که دلتون میخواد یه Assertion قرار میدید تا یک چیزی رو چک کنید (به زبان فرمال، یک ویژگی‌ای که بشه با propositional logic توصیفش کرد رو می‌نویسید). اگر توی کدتون سناریویی وجود داشته باشه که طبق اون Thread ها میتونن Interleave بشن و باعث بشه که Assertion شما نقض بشه، JMC اون سناریو رو پیدا می‌کنه.

اما Strategy هایی که JMC برای Interleave کردن تردها استفاده میکنه ۳ تاست. یکی Random Strategy هست. JMC توی این حالت که به نظرم بشدت بورینگ عه میاد به تعداد دلخواهی که شما مشخص میکنید، برنامه‌تون رو با انتخاب کردن رندوم تردها اجرا میکنه. اگر یک Execution Trace ای باشه که طبق اون برنامه تون به باگ بخوره، اون trace رو بهتون برمی‌گردونه و توی یه فایل ذخیره میکنه.

استراتژی دوم که خیلی جذابه اسمش DPOR-based Stateless Model Checking هست که شما می‌تونید Trust صداش کنید :) داستان اینه که برنامه‌های مالتی ترد شما همه چیزش Finite عه. بنابراین تعداد کل Interleaving های موجود برای تردهای برنامه تون هم محدوده. منتهی بحثی که هست اینه که تعدادشون به شکل انفجاری زیاده و نمیشه تک تک شون رو بررسی کرد. منتهی نکته‌ای که وجود داره اینه که خیلی از این Interleaving ها در انتها result یکسان دارن و به نوعی با هم Equivalent هستند. JMC میاد بر اساس یک سری تئوری مثل Mazurkiewicz Trace Theory و free partially commutative monoid یک Partial order reduction میزنه و به جای اینکه بیاد تک تک Interleaving های ممکن رو جنریت کنه و اجرا کنه، میاد equivalence class های این Interleaving رو میسازه و از هر کدوم یک representative رو اجرا میکنه. اینطوری میشه گفت که به نوعی تمام trace ها رو چک کرده. ساختاری که باهاش این Partial order رو بازنمایی می‌کنیم execution graph هست و JMC برای درک بهتر میاد براتون این گراف ها رو Visualize میکنه و خروجی .dot هم میده.

استراتژی سوم هم Replay هستش که میاد اون Trace باگ داری رو که پیدا شده و ذخیره کرده و مجدد براتون Replay میکنه که برای امر Debugging بسیار مفیده(البته در نسخه‌های آینده میایم بحث Automated Program Repair رو هم بهش اضافه میکنیم).

خلاصه این یه نمایی کلی بود از اون چیزی که JMC انجام میده.

درخواستی که ازتون دارم اینه که این repo رو clone کنید و build کنید و چند تا از سمپل‌هاش رو ران کنید. اگر خوشتون اومد، ممنون میشم به چالش بکشید tool رو.

باور کنید نوشتن برنامه‌های مالتی‌تردی که درست کار کنه خیلی سخت‌تر از اونیه که فکر می‌کنید، JMC این گزاره رو براتون اثبات می‌کنه.

دوستان بنده پاسخ تعدادی از کامنت‌ها رو اینجا می‌نویسم.
۱. ریپو پروژه پابلیکه و طبق لایسنسش (نمی‌دانم، اطلاعی ندارم) می‌تونید کانتریبیوت کنید.
۲. دلیل اینکه Java رو انتخاب کردیم... اولا جاوا تنها زبانی نیست که می‌تونید برنامه‌هاش رو وریفای کنید، ما با مهندسایی توی AWS طرفیم که برنامه‌هاشون رو با زبان‌های JVM-based نوشتن، و خب یه دلیل انتخاب جاوا اینه. دلیل دوم اینه که JVM در طول‌ سال‌های گذشته بسیار Stable تر بوده نسبت به LLVM و خب این باعث میشه که ابزارمون durability بهتری داشته باشه. دلیل سوم این که زبان‌های مبتنی بر JVM جزو Mainstream ها برای نوشتن برنامه‌های Concurrent و Distributed هستند. دلیل چهارم، Bytecode خیلی Abstraction قشنگی ایجاد کرده و باعث میشه ما خیلی درگیر ریزه‌کاری‌های سطح پایین نشیم(مثلا توی C ممکنه لازم باشه شما حتی تا Register Level هم ریز بشی، البته خیلی بدم نمیاد که gcc رو یک سیخی بزنم در آینده). دلیل پنجم، من فعلا فقط JVM بلدم :)
۳. بحث Software Model Checking خیلی قدیمی نیست. اگر بخوام کمی اطلاعات تاریخی بهتون بدم، این بحث برمیگرده به تز دکتری آقای Patrice Godefroid و مقاله‌ی معروف VeriSoft ایشون. بنابراین بحث به نوعی از سال ۱۹۹۷ شروع شد. منتهی خیلی قضیه جدی نبود تا اینکه ایشون سال ۲۰۰۵ یک مقاله‌ای میدن با عنوان Dynamic partial-order reduction for model checking software و به نوعی بحث Model Checking با پیدایش کانسپت DPOR بشدت داغ میشه. توی این دو دهه مقالات بسیار زیادی توی این حوزه اومده که State-of-the-art این حوزه ابزار GenMC با الگوریتم Trust هستش که سال ۲۰۲۲ منتشر شد. کار ما به نوعی بر اساس revisit این کار اخیر هستش.

یکی از دوستان برام اینو فرستاده که مال این کتابه. این خیلی معروفه توی اینترنت و میگن دیس ریاضی‌دانا به CS ای‌هاست. منتهی چون ریاضی‌دانا خیلی شاید با مفهوم Infinite Tree آشنایی ندارن خیلی درکی از اینکه چرا درخت رو اینطوری میکشن هم پیدا نمی‌کنند :)

تو حوزه فرمال، بازه‌ی زمانی بیشتر پیپرهایی که می‌خونی مال حداقل ۴ دهه پیشه. مثلا این مقاله سال ۱۹۷۵ منتشر شده. توی این مقالات بزرگترین چالشی که دهنت رو سرویس میکنه، سبک نوشتاری قرون وسطائی و رسمی نویسنده است. مثلا توی این عکس provided یعنی همون if only ولی اگر اینو ندونی احساس میکنی جمله نویسنده خیلی بی معنی و نامفهومه

متفاعلن متفاعلن متفاعلن متفاعلن

اگر به مباحث Cyber-physcial Systems علاقه مندید و دوست دارید یادبگیرید که چطور فرمال متد میتونه در این حوزه نقش کلیدی بازی کنه بهتون پیشنهاد میکنم که این کورس آقای زمانی رو حتما استفاده کنید. در کنار کورس Sayan Mitra که قبلا توی این پست بهتون معرفی کردم، خیلی مطالب خوبی رو پوشش میده.

I recently launched a Coursera specialization noscriptd "Foundations of Autonomous Systems," which comprises three courses: 1- Modeling of Autonomous Systems; 2- Requirement Specifications for Autonomous Systems; and 3- Verification and Synthesis of Autonomous Systems. This specialization equips learners with the skills to model basic autonomous systems, including linear control systems, sequential circuits, and simple timed automata in a unified framework. Participants will also learn to describe regular or omega-regular expressions, linear temporal logic formulas, and their corresponding automata representations. Additionally, the courses cover conducting model checking for finite systems and synthesizing controllers to meet various requirements such as safety and reachability using fixed-point algorithms. Another key aspect of the specialization is teaching how to construct finite abstractions of continuous-space systems.

PS. You should be able to access the content for free.

https://lnkd.in/gJ-5sGXv

https://lnkd.in/gWbQ2yS2

https://lnkd.in/gamcC_BN

"Non Recursively Enumerable Language is natural"
—————————————————————————

یادمه وقتی که TA درس آتوماتا بودم، یکی از بزرگترین معضلات‌مون سر جلسات امتحان این بود که اگر یک سوالی پیرامون رابطه‌ی زبان‌های Undecidable و non-Turing Recognizable میومد، بچه‌ها حسابی گیج میشدن. و دقیقا یادمه یه نفر ازم پرسید یعنی چی که یک زبان براش Turing پذیرنده نداریم؟ خب این یعنی همون Undecidable دیگه! و خب وقتی هم که بهم می‌گفت یه مثال بگو از یک مسئله‌ای که Non Recursively Enumerable باشه (همون non-Turing Recognizable) هیچ مثال Natural ای به ذهنم نمیرسید و اگر چیزی میگفتم صرفا یک سری مثال انتزاعی بود.

توی آپدیت بعدی JMC قراره که براش قابلیت Symbolic Execution اضافه کنیم و در کنار Concrete Execution سعی کنیم که یک reduction دیگه روی reduction های فعلی بزنیم تا Equivalent Class های Execution Trace ها از اینی که الان هست Coarser تر بشه. اصطلاحا به این تکنیک میگن Concolic و اگر میخواید راجع بهش بخونید این مقاله از Gul Agha رو بخونید. نکته جالبی که توی این قضیه هست اینه که وقتی میخوان برای زبان‌هایی که پوینتر دارن مثل C این تکنیک رو استفاده کنند، مجبورن اون بخش Symbolic pointer analysis رو با approximation حل کنند. و خب دلیلش برام جالب اومد و دنبالش رو گرفتم ببینم قضیه چیه.

قبل از اینکه داستان رو بگم باید یک سری چیزا رو توضیح بدم. اولین نکته اینه که وقتی در طول اجرای یک برنامه یک جایی هست که بیش از یک اسم برای یک آدرس فیزیکی توی حافظه داریم میگیم پدیده‌ی alias رخ داده. مثلا توی زبان C وقتی داریم p = &v یعنی بین p* و v یک alias وجود داره. در حوزه‌ی Static Analysis، یکی از پرسش‌های اساسی Aliasing نام داره. این پرسش یعنی پیدا کردن alias های داخل برنامه به روش Statically. در حقیقت مراد از Static Analysis در اینجا یعنی تحلیل برنامه به واسطه‌ی سینتکس.

حالا ما دو جور Aliasing داریم. یکیش رو میگن May Aliasing که به قول منطق‌کارای Branching-time همون Existential Path عه، یعنی پیدا کردن aliases هایی که در بعضی از اجراهای یک برنامه رخ میدن. دیگری رو هم میگن Must Aliases که همون Universal Path عه، یعنی پیدا کردن aliases هایی که در تمام اجراهای یک برنامه رخ میدن.

حالا میرسیم سر وقت Punch Line قصه : مسئله‌ی اول Undecidable هستش ولی مسئله‌ی دوم non-Turing Recognizable :)) و این یکی از بهترین مثالهایی بود که Natural بودن Non Recursively Enumerable Language ها رو نشون میده. من اگر این رو اون موقع می‌دونستم به اون دوست عزیز سر جلسه‌ی امتحان توضیح میدادم. امیدوارم توی کانالم باشه و بخونه این پست رو :))

آقای William Landi این مسائل رو سال ۱۹۹۲ اثبات میکنند توی این مقاله. ۳ سال بعد آقای Ramalingam یک اثبات ساده تر هم توی این مقاله برای این مسائل پیشنهاد می‌کنند. اگر خیلی بییشتر با این مسائل حال کردید توصیه میکنم این مقاله‌ی آقای Bozga و Iosif رو بخونید. توی این مقاله دو تا لاجیک PAL و WAL رو معرفی میکنند که یک زیرمجموعه‌ای از برنامه رو میتونن با یک روش استنتاجی Aliasing کنند.

یک توصیه‌ای هم دارم برای اون دسته از عزیزانی که توی کانال بنده هستند و این ترم TA درس آتوماتا در جایی‌اند. مقاله‌ی آقای Landi رو بررسی کنید. به نظرم زمانی که درس به مبحث computability و complexity رسید، یه تمرین فوق العاده زیبا که می‌تونید برای دانشجوها طرح کنید اثبات decidable/undecidable بودن مسئله‌ی May Aliasing و Turng Recognizable/non-Recognizable بودن مسئله‌ی Must Aliasing هستش.
هم شیوه‌ی اثباتش قشنگه و هم یک مسئله‌ی Natural عه.

آقا بیاید یه فکت جالب بگم.
مقاله‌ای که دیروز از Bozga و Iosif معرفی کردم یک نویسنده‌ی سومی هم داشت که چون اسمش رو خیلی نشنیده بودم عنوان نکردم. نویسنده‌ی سوم مقاله آقای Yassine Lakhnech هستند که از ابتدای سال جدید میلادی President دانشگاه Université Grenoble Alpes شدند! همون دانشگاهی که سال‌هاست استادش بودند. این دانشگاه یه گروه تحقیقاتی به شدت قوی توی فرمال داره به اسم VERIMAG. این آزمایشگاه توسط آقای Joseph Sifakis بزرگ، برنده‌ی جایزه‌ی تورینگ، احداث شد و ایشون تا موعد بازنشستگی‌شون رییس این آزمایشگاه بودند. به اهل فرمال به شدت توصیه میکنم که سری به سایت این آزمایشگاه بزنند و با بررسی کارهای افراد این گروه کیف کنند.

داشتم فکر میکردم فرمال آدم رو عاقبت بخیر می‌کنه، یکی میشه رییس دانشگاه یکی تورینگ می‌بره. اما AI... بگذریم.

حالا که حرف از VERIMAG شد، شما رو دعوت می‌کنم تا این پست از کانال رو بخونید. توی این پست راجع به یکی از دستاوردهای این گروه صحبت کردیم.

چند روزیه هر کانالی رو رندوم چک میکنم، تبلیغ یک ایونت تو حوزه‌ی تست سافتور میبینم. بخصوص کانالای ریاضی. والا من یه سرچی روی سوابق ارائه دهنده زدم چیز خیلی خاصی پیدا نکردم. کلا هم تو ایران به نظرم اندازه‌ی انگشتان یک دست هم نیستن افرادی که واقعا تست بلد باشن. توصیه‌ام اینه اگر از این ایونت‌های رایگانه که خب شرکت کنید ولی در کل خیلی توقع خاصی ازش نداشته باشید.

اگر می‌خواید تست رو جدی کار کنید حالا چه توی کارای industry و چه academic به نظرم یکی از بهترین منابع Open Access ای که وجود داره دو کتاب هست که سلطان Andreas Zeller نوشته. کتاب‌های The Fuzzing Book و The Debugging Book حاصل سال‌ها تحقیقات و دست‌آوردهای آقای Zeller و تیم شون توی دانشگاه زارلند و موسسه‌ی CISPA است که به نظرم واقعا نیست روی دستش. هر فصل کتاب یه ویدئوی مقدمه هم داره که بهتون یه دید خوبی میده نسبت به مطالب اون فصل. علاوه بر اون کدهای هر دو کتاب با Python زده شده و Notebook هم داره (که البته به نظرم بزرگ‌ترین ضعف کتاب اینه که Multi Lingual نیست).

در کل خیلی پروژه‌ی بکر و درستیه. برخلاف عموم ایونت‌های [غیر]دانشگاهی.

حاج آقا دعا کنند ما آمین بگیم :
May the force of P and NP be with you

از آلبوم جدید نامجو
https://open.spotify.com/track/58iYZYEDdNlVU7eTcH7K4D?si=f1dab86c10a14820

واقعا یکی از بزرگترین اشتباهام پابلیک گذاشتن این کانال بود، به نوعی با این کار کانال رو نابودش کردم. اون زمانی که هر کس میخواست عضو کانال بشه پیام می‌داد رو بیشتر دوست داشتم چون افرادی که می‌خواستن بیان واقعا کنجکاو یا علاقه‌مند بودن، مهم تر از اون باعث میشد که منم بتونم آدمایی که تو حال و هوای خودم سر می‌کنن رو بیشتر بشناسم. برای همین حقیقتا خیلی دیگه دستم به نوشتن تو اینجا نمیره. اینجا پر از آدمایی شده که نمی‌شناسمشون و از اون بدتر فکر میکنن اینم یه کانال آموزش برنامه‌نویسیه و از نظر تفکرات و عقیدتی هم به خط مشی من ذره‌ای نزدیک نیستن. خلاصه ای کاش واقعا دویست سیصد نفر بودیم ولی همه با صفا. خلاصه الان اومدم فقط یه چیزی بگم و برم،

خیلی خیلی قدیما یه بنده خدایی یادمه به من پیام داد که دوست داره تو حوزه‌ی فرمال و NLP کار کنه و ازم میخواست که بهش یه سری آدم معرفی کنم. اون موقع خیلی اطلاعی نداشتم و ایگنور کردم یا بهش گفتم نمی‌دانم. چند وقت پیش منتهی یه Summer School پیدا کردم که هر سال دقیقا توی همین حوزه برگزار میشه و آدمایی که میان لکچر میدن و اتند میکنند اکثرا حوزه کاری‌شون همینه. خلاصه اگر توی کانالم هستی و هنوز لفت ندادی، برو توی این لینک و اسم ارائه دهنده‌ها و متریال لکچرها رو یه بررسی بکن. لینک رویداد های قبلیش رو هم می‌تونی توش پیدا کنی :