آنچه که TLA+ می تواند و نمی تواند بررسی کند

هفته گذشته بوریس چرنی، مخترع کلود کد، اشاره کرد که Opus توانسته از TLA+ 1 برای یافتن شرایط مسابقه در کد استفاده کند.

و اکنون همه در اینترنت در مورد تأیید رسمی صحبت می کنند.

به عنوان یک مربی قدیمی ( 1 2 ) و مدافع TLA+، این واقعا هیجان انگیز است! TLA+ در طراحی سیستم های همزمان پیچیده و اطمینان از اینکه آنها بدون اشکال هستند عالی است. 2 به‌عنوان یک طرفدار دیرینه سرگیجه، این سرخوشی جدید مرا نگران می‌کند. من خیلی ها را خواندم که می گویند روش های رسمی مشکل توسعه نرم افزار عامل را یک بار برای همیشه حل می کند و این مزخرف است.

(این به دانش اولیه TLA+ نیاز دارد. اگر کاملا مبتدی هستید، موارد [1] [2] بالا را بررسی کنید یا اینجا را بخوانید.)

TLA+ سیستم را به مجموعه ای از رفتارها تقسیم می کند. هر رفتار دنباله ای از حالات است، مانند "روشنی سبز، سپس زرد، سپس قرمز". در هر حالت می توانیم عبارات بولی منظمی مانند "نور چهار سبز است" یا "همه چراغ ها قرمز هستند" را بیان کنیم. ما همچنین می توانیم عبارات را با سه عملگر منطقی "زمانی" تغییر دهیم:

وقتی می گوییم P یکی از ویژگی های سیستم است، منظورمان این است که در حالت اولیه هر رفتار درست است. بنابراین اگر ویژگی []P را بررسی کنیم، به این معنی است که []P در هر حالت اولیه درست است، و سپس با تعریف "همیشه" به این معنی است که P در هر حالت آینده از آن حالت اولیه صادق است، یعنی در هر حالت از هر رفتاری صادق است. ما این را یک تغییر ناپذیر می نامیم و یکی از اساسی ترین ویژگی هایی است که در TLA+ بررسی می کنیم.

همچنین می‌توانیم [] را با اعداد اول بنویسیم تا ویژگی‌های عمل را بدست آوریم، یا انواع را تغییر دهیم. [](x' >= x) اگر مقدار جدید x همیشه بزرگتر از مقدار قبلی x باشد، درست است. یکی دیگر از سرگرم کننده ها [](P => P') است: وقتی P درست باشد، دیگر هرگز نمی تواند نادرست شود. TLA+ واقعی به دلیل چیزی به نام "لکنت ناپذیری" کمی پیچیده تر است، اما این جزئیات اضافی است. ویژگی‌های عمل و متغیرهای ثابت، هر دو ویژگی ایمنی هستند، که تقریبا به معنای "چیز بد هرگز اتفاق نمی‌افتد" است. من در اینجا مقاله ای در مورد ایمنی و زندگی نوشتم.

Liveness، btw، «همیشه اتفاق خوبی می افتد». همه خصوصیات زنده بودن بر اساس <> هستند. به خودی خود، <>P فقط به معنای "P در حداقل یک حالت از هر رفتار صادق است" است، که معمولا آنقدر ضعیف است که یک ویژگی سیستم خوب باشد. اما با ترکیب، می‌توانیم خواص زنده‌گی جالب‌تری ایجاد کنیم:

چند عملگر دیگر مانند ENABLED و <<A>>_v وجود دارد که ترفندهای دیگری را باز می‌کنند، اما اکثر مواردی که بررسی می‌کنیم ثابت‌ها، ویژگی‌های اکشن و زنده بودن هستند. و پالایش که ترکیبی از ایمنی و سرزندگی و موضوعی برای خودش است.

بیایید با بدیهی شروع کنیم: اگر نمی دانید چگونه دارایی خود را به عنوان یک فرمول منطقی نشان دهید، TLA+ نمی تواند به شما کمک کند. همچنین هیچ روش رسمی نمی تواند. اگر نتوانید مفهوم انسانی پرنده را رسمی کنید، نمی توانید ثابت کنید که اپلیکیشن شما پرندگان را می شناسد. و، متأسفانه، بسیاری از خواص مهم ما در این دسته قرار می گیرند.

بعد، چیزهای بیش از حد خاص. ویژگی‌های ایمنی TLA+ در سطح حالت‌های جداگانه (غیر متغیر) یا تک مرحله‌ای (ویژگی‌های عمل) کار می‌کنند. شما نمی توانید یک ویژگی را در دو یا چند مرحله به طور بومی تعریف کنید، مانند "فشردن delete و سپس لغو حالت اولیه را به شما برمی گرداند" یا "پس از فشار دادن برق، کامپیوتر در عرض ده مرحله روشن می شود". همچنین نمی‌توانیم ویژگی‌ها را بر روی عملیات ممیز شناور یا در زمان واقعی تعریف کنیم، فقط زمان منطقی.

حالا محدودیتی که بیشتر مورد علاقه من است. ویژگی‌های TLA+ به طور ضمنی در تمام رفتارها اندازه‌گیری می‌شوند. من گفتم که بررسی []P به معنای "P در هر حالت درست است" است، اما معنای واقعی آن این است که "برای همه رفتارها، []P در مورد حالت اولیه آن رفتار صادق است." هر خاصیتی که TLA+ می‌تواند سیستم را بررسی کند، باید ویژگی‌ای باشد که برای هر رفتار فردی صادق باشد.

چه چیزی را از قلم می اندازد؟ خیلی بیشتر از چیزی که انتظار دارید!

به عنوان مثال، ما نمی توانیم "رفتاری وجود دارد که در آن P درست است" انجام دهیم. بنابراین نمی‌توانیم بگوییم که P ممکن است، حتی اگر واقعا به آن نرسیده باشیم. یکی از نمونه های این امر می تواند اثبات برنده بودن یک بازی باشد. ما این ویژگی های دسترسی را می نامیم. ویژگی‌های پیشرفته‌تر دسترسی‌پذیری چیزهایی مانند "P از هر حالت اولیه قابل دسترسی است" یا "P قابل دسترسی از هر حالتی است که Q درست است" است.

همچنین نمی‌توانیم ویژگی‌ها را روی مجموعه‌ای از رفتارها تعریف کنیم. به این می گویند hyperproperty. فرض کنید در حال مدل‌سازی سخت‌افزار تلفن هستیم و می‌خواهیم تأیید کنیم که حالت صرفه‌جویی در مصرف انرژی همیشه انرژی کمتری نسبت به حالت عادی مصرف می‌کند. ویژگی این است که "هر دنباله ای از اقدامات در حالت صرفه جویی در مصرف انرژی بیشتر از حالت عادی استفاده نمی کند." برای رد این موضوع، باید دو رفتار را به من بدهید که یکسان هستند به جز اینکه یکی در حالت صرفه جویی در انرژی شروع می شود و دیگری نه، و حالت معمولی انرژی کمتری مصرف می کند. یک رفتار واحد برای قطع آن کافی نیست، بنابراین بررسی طبیعی آن در TLA+ غیرممکن است.

Hyperproperties ممکن است خاص به نظر برسند، اما آنها تعداد زیادی از ویژگی های امنیتی و تمام ویژگی های آماری را پوشش می دهند ("زمان پاسخ 95% ile 5ms است").

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

وقتی گفتم TLA+ نمی تواند این کارها را انجام دهد، خیلی ساده کردم. منظورم این است که اگر در حال نوشتن یک مشخصات هستید و آن مشخصات مستقیما با سیستمی که می خواهید بسازید مطابقت دارد، TLA+ نمی تواند اینها را به عنوان ویژگی های سیستم شما بیان کند. اما می‌توانید ویژگی‌های دو مرحله‌ای را با متغیرهای کمکی تقلید کنید، مانند ذخیره همه تغییرات حالت در یک دنباله state_history و تعریف ویژگی به عنوان یک متغیر در آن دنباله. می‌توانید برخی از ویژگی‌های فوق‌العاده را با ترکیب خود تقلید کنید، که در آن هر رفتار از مشخصات خود ترکیبی، دو رفتار سیستم واقعی است.

جستجوگر اصلی مدل TLA+ (TLC) می‌تواند ابتدایی‌ترین ویژگی‌های دسترسی را با کلیدواژه جدید REACHABLE و برخی ویژگی‌های فضای حالت را با TLCGet بررسی کند. اندرو هلور یک پست دیوانه کننده در مورد تقلید از "همیشه در دسترس" با انصاف و "بستن ماشین" دارد.

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

همچنین می توانید از ابزار دیگری با تمرکز متفاوت استفاده کنید. CTL می‌تواند ویژگی‌های دسترسی، ویژگی‌های احتمالی PRISM، و غیره را انجام دهد. آنها با بدتر بودن در کارهایی که TLA+ می‌تواند انجام دهد، معامله می‌کنند، و البته هیچ یک از آنها ویژگی‌هایی را که نمی‌توانیم به طور منطقی بیان کنیم، کنترل نمی‌کنند.

در نهایت TLA+ در چیدن بسیاری از میوه های کم آویزان بسیار خوب است و زنده بودن بسیاری از چیزهایی را که ما به آنها اهمیت می دهیم را پوشش می دهد، و TLA+ در بیان و بررسی آنها بسیار خوب است. استفاده از TLA+ برای بررسی کد vibe پتانسیل زیادی (و مشکلات زیادی) دارد. اما چیزهای زیادی وجود دارد که حتی نمی تواند بیان کند، چه رسد به بررسی.

با تشکر از همه کسانی که به پخش زنده هفته گذشته آمدند! شما می توانید کل مطلب را اینجا تماشا کنید.

"منطق زمانی اعمال". این یک زبان مشخصات است که برای یافتن اشکالات در سیستم های همزمان استفاده می شود. در اینجا توضیحی در مورد نام آمده است. ↩

(و در مورد این سوال که چرا یک فرد انجیلی در مورد روش های رسمی به یک شرکت آزمایش ملحق شد، خوب، باید به زودی مقاله ای در وبلاگ آنها در مورد آن وجود داشته باشد.) ↩

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

Logic for Programmers اکنون به صورت چاپی در دسترس است!