Толкова се забавлявах да си играя с TLA+ и Coyote (вижте най-новото), че реших да продължа със сравняването на някои други инструменти за формални методи. Има редица проекти, излизащи от Microsoft Research, и отново можем да използваме проблем „Rosetta Stone“ (който аз свободно определям като нещо, което на теория е лесно за превод между различни езици, което ви позволява да се съсредоточите повече върху разликата в езиците, отколкото съдържанието на проблема). Ако сте експерт по P, можете да преминете към repo на Github. Но ако не знаете своя PSpecот вашия PTest, прочетете нататък.
Първо, искам да поздравя „Хилъл Уейн“. Той не само пише много (книга, онлайн уроци и чест бюлетин!), но също така беше достатъчно добър да ми даде отзиви за няколко от тези експерименти с играчки. Това наистина започва и завършва с него, така че се дължи заслужена заслуга. Благодаря, Хилел!
Хилел наскоро обнови своя уебсайт с уроци learntla.com, който всъщност е книга за изучаване на Pluscal, езикът на разпределения алгоритъм, който може да бъде транскрибиран на TLA+. „Концептуалният преглед“ включва проблем, който също е в книгата на Хилел „Практически TLA+“. Основният проблем е следният: потребител има сметка в банка и иска да може да тегли пари, но никога не иска овърдрафт (официално дефиниран като салдо по сметката под нулата). Как можем да сме сигурни, че потребителят никога не овърдрафтва в едновременна, многонишкова среда?
Грешката в този пример е, че програмата може да проверява условно салдото по банковата сметка едновременно, преди първо да изтегли пари. Балансът може да е наред и за двете заявки за теглене, когато е проверен, но след извършване на двете тегления програмата може да наруши инварианта „без овърдрафти“. Например потребител има $10 и две заявки идват за $10. Програмата проверява и двете, преди да тегли и двете, и казва: „Да, имате $10, давайте!“ Бум. Потребителят вече има салдо по сметката с $10 под нулата. Потребителят е засегнат от такси за овърдрафт, трябва да ипотекира дома си и животът му се спира. Нарушаването на инвариант е лошо!
Хилел има просто решение за този проблем в книгата си: просто се уверете, че чекът и тегленето се случват по едно и също време, в една и съща стъпка от операции, вместо първо чек и после теглене. Това решение ще се появи отново по-късно, докато се боря с прилагането на грешката с P.
P е друг модел за проверка като TLA+. Докато TLA+ може да докаже спецификация, P използва Coyote под капака, за да тества спецификация. Ankush Desai направи „приятен разговор на P“ по време на тазгодишната конференция Strangeloop и има голям брой „уроци“, които могат да ви помогнат да започнете. (Единственият трик е, ако сте следвали и сте използвали Coyote преди, уверете се, че използвате dotnet v3.1 и подходящата версия на Coyote. Има някои предложени решения, ако срещнете проблеми с този проблем с Github. )
Дори и с цялото съдържание на уроците и документацията, трябва да призная: отне ми известно време дори да започна да разбирам какво по дяволите прави P. Този блог от Mohammad Roohitavaf изглеждаше като ръководството за потребителя, което ми липсваше. След като прочетох блога на Mohammad и изгледах отново видеото на Strangeloop, най-накрая успях да атакувам първия примерен проект в P урока — който, колкото и да е смешно, е банков сървър!
Инвариантното нарушение в първото упражнение не е същото като това на Хилел, но ме накара да се чудя... можем ли да пресъздадем грешката от Pluscal в P?
Е… това, което изглежда като обикновен бъг, не беше толкова лесно за мен да внедря. Дори изпратих имейл на Ankush и той беше достатъчно любезен, за да ми отговори. Той отбеляза добре — TLA+ е модел на споделена памет (ETA: Експертът на TLA+ Маркус Купе „се протегна и посочи“, че TLA+ може да има модел на споделена памет, но не се ограничава до него. Благодаря за пояснението, Markus! наистина трябва да бъде, „Примерът Pluscal използва модел на споделена памет.“), докато P използва модела на изчисление, като всяка машина има своя собствена памет. Ключът би бил да се използват събития за достъп до паметта. Както каза Анкуш, „Това е обикновен бъг и трябва да се хване лесно с P.“ Така че защо ми беше трудно да го хвана, дори след имейла на Анкуш?
Докато настройвах банковия урок клиент-сървър, за да опитам това, реших да го изхвърля и да започна отначало. На първо място, стартирането на проект от нулата беше чудесен начин да научите P. Всъщност разбрах структурата на папката P на PSrc, PSpec и PTest. (Бърз преглед на папката: PSrc съхранява клиента, сървъра и събитията; PTest създава програмата, която управлява тестването; PSpec наблюдава поведението на машините и се проваля, ако забележи нещо странно).
Но все пак няма късмет със задействането на грешката! Изпратих имейл на Хилел за помощ и той ми предложи да изпратя събития, за да премина от всяко състояние в друго. О!
Не разбирах нещо фундаментално за P, което е различно от Pluscal. В Pluscal, когато модел преминава между състояние, това се третира като отделна операция. Това не е непременно вярно в P. Помните ли как казах, че решението на Хилел е да обедини чека и тегленето в една и съща операция? Без да искам, това правех!
Виждате ли, P има два начина за преминаване към различни състояния: можете да „отидете“ или можете да „изпратите“ събитие. Goto се случва автоматично и всъщност не разделя кода нагоре - прилагайки „фиксираната“ версия на Hillel, тъй като няма шанс за едновременни проверки с „goto“, изпращайки програмата в различни състояния. С обратната връзка на Хилел, актуализирах модела, за да преход само от състояние със събитие и бум — едновременна лудост. Разгледайте Github тук.
Няма да кажа, че програмата ми е перфектна — многократно изпращам клиентски заявки, за да задействам грешката, докато Pluscal/TLA+/TLC може да улови грешката без множество клиентски заявки. Вероятно има нещо друго, което не разбирам относно P... но това е същата грешка, така че се радвам, че мога да репликирам проблема директно. И нямам нищо против да помоля за помощ... когато става въпрос за официални методи, имам нужда от цялата помощ, която мога да получа!
Какви неща научих? Има някои големи разлики между Pluscal/TLA+ и P. TLA+ използва „стъпки“ като операции, докато P може да превключва между състояния със събитие или директно, по-скоро като извикване на функция. P файловата структура отнема малко време, за да свикнете, което е различно от TLA+, където множество машини могат да бъдат дефинирани в един файл. Предполагам, че на теория множество машини могат да бъдат дефинирани в един файл на P, но може да е дълго и разхвърляно.
Shaz Qadeer даде разговор в Microsoft Research на P, където отбелязва разликите между P и TLA+. Той казва, че TLA+ е висока абстракция над кода и че поддържането на модел заедно с кода е бреме за разработчиците. P се опитва да коригира този „фундаментален проблем“, като създава спецификация, която е много по-близо до кода. Със сигурност виждам, че P е нещо като код и може да се поддържа като код, въпреки че от това, което мога да кажа, има някои предупреждения относно използването на P за генериране на код. Някои проекти обаче го направиха и би си струвало да проучим повече.
Като цяло, това е интересен подход и бих искал да се върна към него. Любимата ми част от изучаването на нови инструменти – особено модели пулове – е, че чувствам, че се научавам как да мисля по нови начини. Наистина ми харесва начинът, по който P ме кара да мисля, особено с тази представа за събитията. Очаквам с нетърпение да науча повече за P и да си поиграя с него. Ако направите нещо с него, уведомете ме!
