Forwarded from Software Engineer Labdon
چطور در معماری میکروسرویس، از ناهماهنگی بین دیتابیس و Message Broker جلوگیری کنیم؟
یکی از چالشهای رایج در میکروسرویسها، تضمین هماهنگی داده (Data Consistency) بین عملیات دیتابیس و ارسال پیام (Event) است.
سناریوی آشنای مشکلساز:
سرویس سفارش (Order) را در نظر بگیرید:
1. سفارش جدید در دیتابیس ذخیره میشود. (موفق)
2. قرار است یک رویداد OrderCreated به Kafka یا RabbitMQ ارسال شود تا سرویس نوتیفیکیشن به کاربر ایمیل بزند. (ناموفق)
نتیجه: سفارش در سیستم ثبت شده، اما به دلیل قطعی موقت در Message Broker، ایمیل تأیید هرگز ارسال نمیشود! این یعنی یک ناهماهنگی جدی در سیستم.
راهحل: الگوی Outbox Pattern
الگوی Outbox یک راهحل زیبا و قابل اعتماد برای این مشکل است. به جای ارسال مستقیم پیام، آن را در یک جدول به نام outbox در همان دیتابیس و داخل همان تراکنش ذخیره میکنیم.
چرا این روش کار میکند؟
چون ذخیره سفارش و ذخیره پیام در جدول
سپس، یک پردازشگر پسزمینه (Message Relay) مسئول خواندن پیامها از جدول outbox و ارسال مطمئن آنها به Message Broker است.
<Mahdi M./>
یکی از چالشهای رایج در میکروسرویسها، تضمین هماهنگی داده (Data Consistency) بین عملیات دیتابیس و ارسال پیام (Event) است.
سناریوی آشنای مشکلساز:
سرویس سفارش (Order) را در نظر بگیرید:
1. سفارش جدید در دیتابیس ذخیره میشود. (موفق)
2. قرار است یک رویداد OrderCreated به Kafka یا RabbitMQ ارسال شود تا سرویس نوتیفیکیشن به کاربر ایمیل بزند. (ناموفق)
نتیجه: سفارش در سیستم ثبت شده، اما به دلیل قطعی موقت در Message Broker، ایمیل تأیید هرگز ارسال نمیشود! این یعنی یک ناهماهنگی جدی در سیستم.
راهحل: الگوی Outbox Pattern
الگوی Outbox یک راهحل زیبا و قابل اعتماد برای این مشکل است. به جای ارسال مستقیم پیام، آن را در یک جدول به نام outbox در همان دیتابیس و داخل همان تراکنش ذخیره میکنیم.
چرا این روش کار میکند؟
چون ذخیره سفارش و ذخیره پیام در جدول
outbox، هر دو در یک تراکنش اتمیک (Atomic Transaction) انجام میشوند. این یعنی یا هر دو با هم موفق میشوند یا هر دو با هم شکست میخورند. به این ترتیب، هیچ رویدادی گم نخواهد شد!سپس، یک پردازشگر پسزمینه (Message Relay) مسئول خواندن پیامها از جدول outbox و ارسال مطمئن آنها به Message Broker است.
<Mahdi M./>
Forwarded from Gopher Academy
شروع یک پروژه Go همیشه با یک سؤال مهم همراهه:
ساختار پروژه رو چطور طراحی کنیم؟
یکی از چالشهای اولیه در پروژههای گولنگ، انتخاب یک ساختار ماژولار، خوانا و مقیاسپذیره. الکس ادواردز در مقالهی زیر، ۱۱ نکته کاربردی برای ساختاردهی پروژههای Go مطرح کرده که خوندنش میتونه توی این مورد بهمون کمک کنه:
https://www.alexedwards.net/blog/11-tips-for-structuring-your-go-projects
<Abbas Pourhadi/>
ساختار پروژه رو چطور طراحی کنیم؟
یکی از چالشهای اولیه در پروژههای گولنگ، انتخاب یک ساختار ماژولار، خوانا و مقیاسپذیره. الکس ادواردز در مقالهی زیر، ۱۱ نکته کاربردی برای ساختاردهی پروژههای Go مطرح کرده که خوندنش میتونه توی این مورد بهمون کمک کنه:
https://www.alexedwards.net/blog/11-tips-for-structuring-your-go-projects
<Abbas Pourhadi/>
Forwarded from Linuxor ?
لینکدین یه بخشی به اسم Skill Assessments داره که توش میتونی آزمونهایی توی موضوعات مختلف (مثلاً Python، JavaScript، Excel، SQL، و غیره) بدی تا نشون بدی توی اون مهارت خاص حرفهای هستی، این لیست همه سوال ها و جوابشون رو جمع کرده :
ebazhanov.github.io/linkedin-skill-assessments-quizzes
@Linuxor
ebazhanov.github.io/linkedin-skill-assessments-quizzes
@Linuxor
Forwarded from دبیان فارسی (Sohrab)
دبیان ۱۳ با نام رمز «تریکسی» روز شنبه ۱۸ مرداد ۱۴۰۴ منتشر خواهد شد.
این تاریخ زودتر از زمانیه که خودمون انتظار داشتیم؛ ولی تصمیم بر این شد که انتشار رو بیخودی عقب نندازیم. از این رو از یکشنبه ۵ مرداد فرایند تثبیت کامل بستهها رو خواهیم داشت و هیچ بستهای جز برای رفع مشکلات بحرانی بهروز نخواهد شد.
برای کمک به ما میتونید فرایند ارتقا رو طبق این راهنما امتحان کنید و مشکلات رو با reportbug upgrade-reports گزارش بدید:
https://wiki.ubuntu-ir.org/wiki/%D8%A7%D8%B1%D8%AA%D9%82%D8%A7%DB%8C_%D8%AF%D8%A8%DB%8C%D8%A7%D9%86
این تاریخ زودتر از زمانیه که خودمون انتظار داشتیم؛ ولی تصمیم بر این شد که انتشار رو بیخودی عقب نندازیم. از این رو از یکشنبه ۵ مرداد فرایند تثبیت کامل بستهها رو خواهیم داشت و هیچ بستهای جز برای رفع مشکلات بحرانی بهروز نخواهد شد.
برای کمک به ما میتونید فرایند ارتقا رو طبق این راهنما امتحان کنید و مشکلات رو با reportbug upgrade-reports گزارش بدید:
https://wiki.ubuntu-ir.org/wiki/%D8%A7%D8%B1%D8%AA%D9%82%D8%A7%DB%8C_%D8%AF%D8%A8%DB%8C%D8%A7%D9%86
Forwarded from محتوای آزاد سهراب
گلچین روزگار چه بد سلیقه است.....
اینتل توزیع clearlinux رو توسعش رو متوقف کرده.
https://www.phoronix.com/news/Intel-Ends-Clear-Linux
اینکه اسمش ررو نشنیده بودید تا الان نگران نباشید، چون حتی دانلودش هم نمیتونستید بکنید میفرستادتون دنبال نخودسیاه.
@SohrabContents
اینتل توزیع clearlinux رو توسعش رو متوقف کرده.
https://www.phoronix.com/news/Intel-Ends-Clear-Linux
اینکه اسمش ررو نشنیده بودید تا الان نگران نباشید، چون حتی دانلودش هم نمیتونستید بکنید میفرستادتون دنبال نخودسیاه.
@SohrabContents
Phoronix
Intel Announces It's Shutting Down Clear Linux
The most depressing news of the week: Intel is ending their performance-optimized Clear Linux distribution
Forwarded from Curious Geek ⚡️
🎉 ورژن نخست چت بات وال ای ریلیز شد
✔️ هروقت دلتون بخواد میتونید صداش کنید
✔️ می تونید باهاش چت کنید
✔️ می تونید ازش راجب فیلم - سریال و موزیک سوال بپرسید
قانون اصلی: حرف فنی ممنوع.
🍃🙂
🆔 @TheGeeksCommunity
✔️ هروقت دلتون بخواد میتونید صداش کنید
✔️ می تونید باهاش چت کنید
✔️ می تونید ازش راجب فیلم - سریال و موزیک سوال بپرسید
قانون اصلی: حرف فنی ممنوع.
🍃🙂
🆔 @TheGeeksCommunity
Forwarded from Gopher Academy
🧭 راهنمای ساختاربندی پروژههای Go
1. ساختار را بر اساس نیاز پروژه انتخاب کنید
سبکهای ساختاری بسته به نوع پروژه (CLI، کتابخانه، وباپ/میکروسرویس) متفاوت است و «یک ساختار برتر» وجود ندارد .
2. کارآمدی مهمتر از کمال
هدف این باشد که ساختار پروژه قابل فهم، قابل تغییر و قابل نگهداری باشد؛ نه لزوماً کامل و بینقص .
3. از روی عادت به ساختار زبانهای دیگر نقل رعایت نکنید
اGo فلسفهٔ ساده خود را دارد؛ تقلید ساختار Django یا Rails ممکن است منجر به سردرگمی شود .
4. هر پوشه=هر package
ایجاد فولدر فقط به دلیل نظم ظاهری اشتباه است. فقط هنگامی package بسازید که منطق مستقلی بخواهید .
5. با یک skeleton استاندارد شروع کنید
پروژههای کوچک: همهٔ فایلها در روت
main.go, foo.go, bar.go
وقتی پکیجهای داخلی نیاز بود:
internal/foo/foo.go
main.go
پروژههای بزرگتر با چند executable:
cmd/app1/, cmd/app2/, internal/, go.mod, README.md
6. اجازه دهید ساختار با رشد پروژه تغییر کند
نیاز به تغییر ساختار را با توسعه واقعی پروژه شناسایی کنید؛ نه از ابتدا همهچیز را طراحی کنید .
7. اگر بلاتکلیف هستید، با دو فایل شروع کنید
فقط go.mod و main.go؛ باقی را با نیاز واقعی اضافه کنید .
8. موارد مرتبط را در کنار هم نگه دارید
توابع کمکی، typeها و متدها مرتبط را نزدیک هم نگه دارید تا خوانایی بیشتر شود .
9. اندازه فایل مهم نیست، تا وقتی درست است
فایلهای بزرگ ایرادی ندارند، مگر اینکه واقعا نگهداری را سخت کنند .
10. پکیجسازی فقط وقتی لازم باشد
پکیجهای خیلی کوچک یا کماهمیت اضافه نکنید؛ مگر برای استفاده مجدد یا جداسازی لایهها .
11. به علائم هشدار توجه کنید
مشکل در پیدا کردن کد
تغییرات کوچک توزیعشده در کل پروژه
پیچیدگی در debugging
وابستگیهای دورانی و مشکل در error handling
→ وقت بازنگری ساختار است .
⚡ جمعبندی
هدف: ساختاری موثر، خوانا، و قابل نگهداری.
روش:
1. شروع ساده،
2. استفاده از ساختار پیشنهادی (مثل پوشههای cmd/, internal/)،
3. اجازه دهید پروژه رشد کند و ساختار با آن عینا وفق پیدا کند.
هشدار: وقتی احساس کردید ساختار کارآمد نیست، فکری برای بازطراحی آن بکنید.
https://t.iss.one/addlist/QtXiQlynEJwzODBk
1. ساختار را بر اساس نیاز پروژه انتخاب کنید
سبکهای ساختاری بسته به نوع پروژه (CLI، کتابخانه، وباپ/میکروسرویس) متفاوت است و «یک ساختار برتر» وجود ندارد .
2. کارآمدی مهمتر از کمال
هدف این باشد که ساختار پروژه قابل فهم، قابل تغییر و قابل نگهداری باشد؛ نه لزوماً کامل و بینقص .
3. از روی عادت به ساختار زبانهای دیگر نقل رعایت نکنید
اGo فلسفهٔ ساده خود را دارد؛ تقلید ساختار Django یا Rails ممکن است منجر به سردرگمی شود .
4. هر پوشه=هر package
ایجاد فولدر فقط به دلیل نظم ظاهری اشتباه است. فقط هنگامی package بسازید که منطق مستقلی بخواهید .
5. با یک skeleton استاندارد شروع کنید
پروژههای کوچک: همهٔ فایلها در روت
main.go, foo.go, bar.go
وقتی پکیجهای داخلی نیاز بود:
internal/foo/foo.go
main.go
پروژههای بزرگتر با چند executable:
cmd/app1/, cmd/app2/, internal/, go.mod, README.md
6. اجازه دهید ساختار با رشد پروژه تغییر کند
نیاز به تغییر ساختار را با توسعه واقعی پروژه شناسایی کنید؛ نه از ابتدا همهچیز را طراحی کنید .
7. اگر بلاتکلیف هستید، با دو فایل شروع کنید
فقط go.mod و main.go؛ باقی را با نیاز واقعی اضافه کنید .
8. موارد مرتبط را در کنار هم نگه دارید
توابع کمکی، typeها و متدها مرتبط را نزدیک هم نگه دارید تا خوانایی بیشتر شود .
9. اندازه فایل مهم نیست، تا وقتی درست است
فایلهای بزرگ ایرادی ندارند، مگر اینکه واقعا نگهداری را سخت کنند .
10. پکیجسازی فقط وقتی لازم باشد
پکیجهای خیلی کوچک یا کماهمیت اضافه نکنید؛ مگر برای استفاده مجدد یا جداسازی لایهها .
11. به علائم هشدار توجه کنید
مشکل در پیدا کردن کد
تغییرات کوچک توزیعشده در کل پروژه
پیچیدگی در debugging
وابستگیهای دورانی و مشکل در error handling
→ وقت بازنگری ساختار است .
⚡ جمعبندی
هدف: ساختاری موثر، خوانا، و قابل نگهداری.
روش:
1. شروع ساده،
2. استفاده از ساختار پیشنهادی (مثل پوشههای cmd/, internal/)،
3. اجازه دهید پروژه رشد کند و ساختار با آن عینا وفق پیدا کند.
هشدار: وقتی احساس کردید ساختار کارآمد نیست، فکری برای بازطراحی آن بکنید.
https://t.iss.one/addlist/QtXiQlynEJwzODBk
Forwarded from DevTwitter | توییت برنامه نویسی
این چند وقته با تحریم خیلی مشکل داشتم، یه ابزار کوچیک نوشتم توش dns هایی که تونستم واسه رفع تحریم پیدا کنم رو گذاشتم که اتوماتیک بینشون میتونین سویچ کنین. اگه خواستین میتونین استفاده کنین
https://github.com/itpourya/beshkan
@DevTwitter | <پوریا/>
https://github.com/itpourya/beshkan
@DevTwitter | <پوریا/>
Forwarded from کانال اطلاعرسانی توزیع پارچ
در بیلد بعدی پارچ، نشست X11 از گنوم و کیدیای پلاسما حذف میشود.
این عمل از سوی بستهبندی بالادستی آرچ رخ میدهد، در کیدیای به صورت دستی میتوانید مجدداً X11 را فعال کنید.
همچنین نگارشهای سنتی نیز مانند XFCE پارچ همراه با labwc و پشتیبانی از ویلند منتشر میشوند.
@ParchLinux
این عمل از سوی بستهبندی بالادستی آرچ رخ میدهد، در کیدیای به صورت دستی میتوانید مجدداً X11 را فعال کنید.
همچنین نگارشهای سنتی نیز مانند XFCE پارچ همراه با labwc و پشتیبانی از ویلند منتشر میشوند.
@ParchLinux
Forwarded from New Elizaium
" تخفیف ویژه ChatGPT Plus "
فقط برای صرفا این یک ماه آینده که امتحانات و پروژه ها و پایان نامه ها ... نزدیک هست !
۱ ماهه اشتراکی - یک دستگاه : 285t
۳ ماهه اشتراکی - یک دستگاه : 697t
۶ ماهه اشتراکی - یک دستگاه : 1.247t
* بدون هیچگونه بن و ارور Suspicious *
جهت تهیه ، رزرو و کسب اطلاعات بیشتر : @ElizaiumHelp
فقط برای صرفا این یک ماه آینده که امتحانات و پروژه ها و پایان نامه ها ... نزدیک هست !
۱ ماهه اشتراکی - یک دستگاه : 285t
۳ ماهه اشتراکی - یک دستگاه : 697t
۶ ماهه اشتراکی - یک دستگاه : 1.247t
* بدون هیچگونه بن و ارور Suspicious *
جهت تهیه ، رزرو و کسب اطلاعات بیشتر : @ElizaiumHelp
❤1
Forwarded from 🎄 یک برنامه نویس تنبل (Lazy 🌱)
Forwarded from SoniaCircuit (Sonia Fatholahi)
This media is not supported in your browser
VIEW IN TELEGRAM
Forwarded from DevTwitter | توییت برنامه نویسی
یک اسکریپت پیدا کردم که قابلیت ساخت Appimage از بستههای نصب شده آرچ رو به شما میده، این اسکریپت در مواقع قطعی اینترنت بینالملل میتونه برای افراد کاربردی باشه که بتونن برنامههایی که نصب داشتن رو با بقیه به عنوان یک بسته Appimage به اشتراک بذارن.
https://github.com/ivan-hc/Arch-Deployer
@DevTwitter | <Sohrab Behdani/>
https://github.com/ivan-hc/Arch-Deployer
@DevTwitter | <Sohrab Behdani/>
Forwarded from CleverDevs (Mammad)
لاراگرام یه فریمورک برای توسعه ربات تلگرامه که توسط امیرحسین با الهام گرفتن از فریمورک لاراول توسعه داده شده که اکثر فیچر های مورد نیاز برای ساخت ربات تلگرامی رو داره که میتونید یه نگاه به گیتهابش بندازید و اگه خوشتون اومد استفاده کنید
https://github.com/laraXgram/LaraGram
@CleverDevs - @CleverDevsGp
https://github.com/laraXgram/LaraGram
@CleverDevs - @CleverDevsGp
Forwarded from Gopher Academy
🔵 عنوان مقاله
Kubernetes Best Practices 2025: Comprehensive White Paper
🟢 خلاصه مقاله:
مقالهای در مورد بهبود امنیت، قابلیت اطمینان و کنترل هزینه در کلاسترهای Kubernetes با استفاده از راهنماییهای عملی بر اساس تجربیات واقعی ارائه شده است. در بخش امنیت، تاکید بر سیاستهای شبکه، بروزرسانیهای منظم و مکانیزمهای دسترسی امن است. برای قابلیت اطمینان، طراحی برای مقابله با شکست و استفاده از استراتژیهایی مانند خودترمیمی و استقرار در چندین منطقه پیشنهاد شده است. نیز، کنترل هزینهها از طریق بهینهسازی استفاده از منابع و پیادهسازی سیستمهای کارآمد لاگبرداری و نظارت تأکید شده است. این راهکارها به کاربران Kubernetes کمک میکنند تا امنیت، قابلیت اطمینان و کفایت هزینه در کلاسترهای خود را بهبود بخشند.
🟣لینک مقاله:
https://golangweekly.com/link/171853/web
➖➖➖➖➖➖➖➖
👑 @gopher_academy
Kubernetes Best Practices 2025: Comprehensive White Paper
🟢 خلاصه مقاله:
مقالهای در مورد بهبود امنیت، قابلیت اطمینان و کنترل هزینه در کلاسترهای Kubernetes با استفاده از راهنماییهای عملی بر اساس تجربیات واقعی ارائه شده است. در بخش امنیت، تاکید بر سیاستهای شبکه، بروزرسانیهای منظم و مکانیزمهای دسترسی امن است. برای قابلیت اطمینان، طراحی برای مقابله با شکست و استفاده از استراتژیهایی مانند خودترمیمی و استقرار در چندین منطقه پیشنهاد شده است. نیز، کنترل هزینهها از طریق بهینهسازی استفاده از منابع و پیادهسازی سیستمهای کارآمد لاگبرداری و نظارت تأکید شده است. این راهکارها به کاربران Kubernetes کمک میکنند تا امنیت، قابلیت اطمینان و کفایت هزینه در کلاسترهای خود را بهبود بخشند.
🟣لینک مقاله:
https://golangweekly.com/link/171853/web
➖➖➖➖➖➖➖➖
👑 @gopher_academy
Fairwinds
Kubernetes Best Practices Resource
Get the updated Kubernetes best practices whitepaper for advice on Kubernetes security, reliability, efficiency, policy and monitoring.
Forwarded from Gopher Academy
Graceful Goroutine Shutdowns in Go: A Practical Guide
https://dev.to/jones_charles_ad50858dbc0/graceful-goroutine-shutdowns-in-go-a-practical-guide-2b9a
https://dev.to/jones_charles_ad50858dbc0/graceful-goroutine-shutdowns-in-go-a-practical-guide-2b9a
DEV Community
Graceful Goroutine Shutdowns in Go: A Practical Guide
Hey there, Go developer! If you’ve been writing Go for a year or two, you’re probably comfy with...
Forwarded from a pessimistic researcher (Kc)
همه اینا رو گفتم که بگم ایونت گرامیداشت ایشون به صورت آنلاین هم برگزار میشه و شما میتونید از طریق لینک zoom ای که روی وبسایت گذاشتن وارد بشید و در جلسات این ایونت شرکت کنید.
این ایونت فردا برگزار میشه و به وقت ایران از ساعت ۱۰:۳۰ صبح شروع و تا ساعت ۷:۳۰ عصر هم ادامه خواهد داشت
این ایونت فردا برگزار میشه و به وقت ایران از ساعت ۱۰:۳۰ صبح شروع و تا ساعت ۷:۳۰ عصر هم ادامه خواهد داشت
Forwarded from a pessimistic researcher (Kc)
گرامیداشت Symbolic Model Checking
————————————
توی کنفرانس CAV یه ایونت ورکشاپ مانندی ترتیب دیدن برای گرامی داشت و تقدیر از زحمات آقای Kenneth McMillan، کسی که بیشک اگر نبود، نه CAV بود و شاید نه Software Model Checking به معنای امروز. ایشون تقریبا اولین کسی بود که با ارائهی یک تکنیک خلاقانه، راهی جدید برای مقابله با State Space Explosion ارائه کرد. مسئله به زبان ساده بدین صورته : مدل چکینگ کلاسیک ایدهاش این بود که ما بیایم تمامی رفتارهای ممکن یک سیستم رو در قالب یک state machine محاسبه کنیم. یعنی یک گراف با مجموعهای از state های اولیه و پایانی و میانی و تعدادی یال یا transition بینشون. در نتیجه میشد مسئلهی verification سیستم رو به مسئلهی Graph Reachability تقلیل داد. در وهلهی اول به نظر میومد که این تکنیک بسیار موثر باشه، چرا که مسئلهی graph reachability یک مسئلهی polynomial هستش و میشه به راحتی حلش کرد. اما چیزی نگذشت که دانشمندان در اون دوران فهمیدن که فضا حالت یک سیستم میتونه به قدری بزرگ باشه که در وهلهی اول اصلا نشه اون فضای حالت رو ذخیره و بازنمایی کرد و در وهله دوم اگر این کار رو هم بکنن، پروسهی reachability تا پایان عمرشون هم به پایان نمیرسه. تصور کنید که یک برنامهی ساده دارید که داخلش یک آرایه به سایز ۱۰ از تایپ int تعریف کردید و هیچ متغیر دیگهای تو برنامه تون وجود نداره. با فرض اینکه هر متغیر int اندازهاش تو حافظه ۳۲ بیت باشه، میتونه
2^32
مقدار مختلف رو بپذیره. حالا شما نه یکی که ده تا دارید و فضای حالت تون معادل
(2^32)^10
حالت میشه. تازه ما تعداد transition هاش رو هم حساب نکردیم.
آقای McMillan با یک ایدهی جدید میان و سعی میکنن که تمام state ها و transition های یک سیستم رو در قالب تعداد محدودی فرمول logical نمایش بدن. بنابراین مشکل اول رو حل کردن یعنی ما حالا میتونستیم به راحتی فضای حالت یک سیستم رو بازنمایی و ذخیره کنیم. در حقیقت ایشون اومدن و مسئلهی Graph Reachability رو به مسئلهی Satisfiablity فرمولهای logical تقلیل دادن.
از اونجایی که ما تو دپارتمانهای CS مون اثبات کردیم که مسئلهی SAT روی منطق گزارهای NP-complete هستش و روی منطق First-order تصمیم ناپذیره، پیش خودمون گفتیم که پس قرار نیست که یک SAT Solver ای روزی ساخته بشه که ما بهش فرمول لاجیکال رو بدیم و اون بهمون بگه که آیا SAT هست یا نه. منتهی یه سریا بودن که توی دپارتمان برق بودن و خیلی به حرفای ما باور نداشتن و شروع با ساختن SAT Solver ها کردند و اون جنبش باعث شد که امروزه SAT و SMT solver هایی داشته باشیم که بسیار خوب و قوی دارن کار میکنن.
به لطف جنبش دپارتمان برقیها امروزه کارای آقای McMillan بیشتر مورد توجه قرار گرفته. چرا که دانشمندان در اون زمان بر این باور بودند که راهکار آقای McMillan فقط مشکل اول مدل چکینگ کلاسیک رو حل کرده و مشکل دوم هنوز سر جاشه. ولی خب به لطف جنبش دپارتمان برقیها اون مشکل تا حد خوبی حل شده و اکثر تکنیکهای مدل چکینگ تو حوزه هاردور و سافتور بر اساس ایدههای ایشون ساخته میشه.
————————————
توی کنفرانس CAV یه ایونت ورکشاپ مانندی ترتیب دیدن برای گرامی داشت و تقدیر از زحمات آقای Kenneth McMillan، کسی که بیشک اگر نبود، نه CAV بود و شاید نه Software Model Checking به معنای امروز. ایشون تقریبا اولین کسی بود که با ارائهی یک تکنیک خلاقانه، راهی جدید برای مقابله با State Space Explosion ارائه کرد. مسئله به زبان ساده بدین صورته : مدل چکینگ کلاسیک ایدهاش این بود که ما بیایم تمامی رفتارهای ممکن یک سیستم رو در قالب یک state machine محاسبه کنیم. یعنی یک گراف با مجموعهای از state های اولیه و پایانی و میانی و تعدادی یال یا transition بینشون. در نتیجه میشد مسئلهی verification سیستم رو به مسئلهی Graph Reachability تقلیل داد. در وهلهی اول به نظر میومد که این تکنیک بسیار موثر باشه، چرا که مسئلهی graph reachability یک مسئلهی polynomial هستش و میشه به راحتی حلش کرد. اما چیزی نگذشت که دانشمندان در اون دوران فهمیدن که فضا حالت یک سیستم میتونه به قدری بزرگ باشه که در وهلهی اول اصلا نشه اون فضای حالت رو ذخیره و بازنمایی کرد و در وهله دوم اگر این کار رو هم بکنن، پروسهی reachability تا پایان عمرشون هم به پایان نمیرسه. تصور کنید که یک برنامهی ساده دارید که داخلش یک آرایه به سایز ۱۰ از تایپ int تعریف کردید و هیچ متغیر دیگهای تو برنامه تون وجود نداره. با فرض اینکه هر متغیر int اندازهاش تو حافظه ۳۲ بیت باشه، میتونه
2^32
مقدار مختلف رو بپذیره. حالا شما نه یکی که ده تا دارید و فضای حالت تون معادل
(2^32)^10
حالت میشه. تازه ما تعداد transition هاش رو هم حساب نکردیم.
آقای McMillan با یک ایدهی جدید میان و سعی میکنن که تمام state ها و transition های یک سیستم رو در قالب تعداد محدودی فرمول logical نمایش بدن. بنابراین مشکل اول رو حل کردن یعنی ما حالا میتونستیم به راحتی فضای حالت یک سیستم رو بازنمایی و ذخیره کنیم. در حقیقت ایشون اومدن و مسئلهی Graph Reachability رو به مسئلهی Satisfiablity فرمولهای logical تقلیل دادن.
از اونجایی که ما تو دپارتمانهای CS مون اثبات کردیم که مسئلهی SAT روی منطق گزارهای NP-complete هستش و روی منطق First-order تصمیم ناپذیره، پیش خودمون گفتیم که پس قرار نیست که یک SAT Solver ای روزی ساخته بشه که ما بهش فرمول لاجیکال رو بدیم و اون بهمون بگه که آیا SAT هست یا نه. منتهی یه سریا بودن که توی دپارتمان برق بودن و خیلی به حرفای ما باور نداشتن و شروع با ساختن SAT Solver ها کردند و اون جنبش باعث شد که امروزه SAT و SMT solver هایی داشته باشیم که بسیار خوب و قوی دارن کار میکنن.
به لطف جنبش دپارتمان برقیها امروزه کارای آقای McMillan بیشتر مورد توجه قرار گرفته. چرا که دانشمندان در اون زمان بر این باور بودند که راهکار آقای McMillan فقط مشکل اول مدل چکینگ کلاسیک رو حل کرده و مشکل دوم هنوز سر جاشه. ولی خب به لطف جنبش دپارتمان برقیها اون مشکل تا حد خوبی حل شده و اکثر تکنیکهای مدل چکینگ تو حوزه هاردور و سافتور بر اساس ایدههای ایشون ساخته میشه.
❤1