[Russian] Как своевременно лочить ресурсы в Макдоналдсе

Я пытался об этом рассказать тут в начале, но невнятно как-то получилось.

Где это еще могло произойти со мной, как не в Одессе? Рядом с Привозом? Впрочем, тот Макдоналдс ближе к ЖД, но за ЖД сразу Привоз, так что, "почти".

То-ли из-за карантина, то-ли это началось раньше, но в Макдоналдсах появились большие дисплеи для самостоятельного выбора блюд. Их там называют "терминалы самообслуживания". Нужно там понажимать на картинки, взять пластиковый номерок в форме кирилличной буквы "Л", ввести его номер, приложить креду. Потом вы выбираете столик, садитесь, ставите номерок на видное место, персонал приходит, ищет ваш номерок, ставит поднос, забирает номерок и уходит.

Выглядит так: 1, 2. (На фотке не я, фотки отсюда. )

Но девайс для заказа симметричный, дисплеи с двух сторон, и номерок тоже симметричный. И в тот день там была толпа. Оказалось, что когда я вводил всё желаемое, и ввел номер на номерке, на другой стороне девайса стоял некий мужик и делал всё ровно то же самое, и ввел тот же номер, потому что перед его глазами был тот же номерок, они висят на перекладине между девайсами.

Примерно в одно и то же время, в пределах нескольких секунд, мы приложили креды, получили чек, и мужик успел взять пластиковый номерок раньше меня, развернулся и на моих глазах ушел в толпу. Я в панике погнал за ним (иначе, как в этой толпе мне принесут заказ?), требуя отдать, мужик начал сопротивляться. Я показал ему выбитый чек, где указан номер этого номерка. Мужик показал мне свой чек, где был указан тот же номер. Мы пошли искать персонал данного заведения, дабы разрулить конфликт. Персонал выслушал нас и сказал, что видит такое первый раз в жизни. Нам с мужиком пришлось сесть рядом, с этим номерком, и ждать когда принесут и ему и мне.

Девайс должен был отдать ошибку, он не должен был допустить ввода одного и того же номера 2 раза подряд, в пределах какого-то разумного времени, например. То-ли он этого не проверяет, то-ли проверяет, и если ввести второй раз слишком быстро, он глючит. Наиболее любознательные читатели моего блога могут попытаться проверить это самостоятельно -- в пределах 1-2 секунды вводить один и тот же номер. Что будет? Я не знаю, мне лень проверять.

Теперь приходится "лочить" вручную: в начале хватаю номерок в руки, потом вбиваю его номер в девайс и с тех пор рассказываю всем, как важно своевременно лочить ресурсы.

Как всегда, выглядит всё это просто, но решить такую проблему труднее, чем кажется. В обычном программировании эти заботы обыкновенно перекладывают на СУБД, даже в MySQL есть разные варианты локов... В случае с Маком, должна была быть какая-то общая база/таблица, где велся бы учет временно зарегестрированных номерков, и чтобы они проверялись при вводе. А может так и есть? Может они и проверяются, но где-то что-то отлетает по таймауту, когда два запроса в базу о добавлении номера приходят слишком быстро? Может быть, база есть, но работает слишком медленно?

И это Макдоналдс, ничего страшного не произошло бы, можно только посмеяться и написать пост в блог, вроде этого. Но представьте авиакомпанию: никто не захочет продать один и тот же билет 2 раза подряд. Ни один банк не захочет списать деньги со счета 2 раза подряд. Да впрочем и люди тоже не хотят, чтобы с их кред списывали деньги 2 раза подряд. Ну и т.д.

Многие украинские автобусные компании, при заказе билета, предлагают выбрать место в автобусе. Что если 2 человека одновременно выберут одно место?

Еще один пример из жизни -- в октябре-2021 власти Киева объявили, что Киев опять переходит в красную зону, и в метро нельзя будет ездить без хотя бы одной вакцины. Народ толпой спешно ломанулся вакцинировться, включая автора сих строк. На одном из сайтов, нужно было выбрать место для вакцинации (один из крупных ТРЦ), и время. Для каждого человека -- свое время, слот в районе 10-15 минут, насколько я помню. Конечно, на сайт ломанулось много людей и эти слоты то появлялись, то пропадали, и даже когда слот был доступен, в конце иногда выдавалась ошибка, что кто-то другой уже успел заполнить анкету раньше. Так или иначе, в самом ТРЦ, в очередях, выяснялось, что на один и тот же временной слот приходили несколько человек -- успели зарегистрироваться и сайт не отдал ошибку. Конечно, сайт сырой -- с этим карантином и резким наплывом желающих вакцинироваться, те IT-шники не успевают делать всё как надо. Опять же, всё обошлось, люди и медики только потратили немного больших времени и своих нервов. Но в некоторых других отраслях последствия от таких ошибок могут быть куда хуже.

А теперь представьте, какой ад бывает в ERP-системах, с документооборотом, где много клиентов, серверов, всё размазано по миру. Или любую соц.сеть уровня facebook...

Такие баги очень неприятные, они проявляются только при большой нагрузке, когда много клиентов, все лезут толпой без очереди, итд. Далеко не всегда такую ситуацию можно воспроизвести заново.

Собственно, model checking и предназначен для решения таких сложностей -- они бывают значительно труднее, чем можно представить. В известной книге Таненбаума про ОС есть немного о том, как ОС разруливает локи и конфликты на уровне ресурсов самой ОС, и всё это непросто.

SAT/SMT-солверы используют как движки, в которых и происходит бОльшая часть работы.


List of my other blog posts.