1. Куча / Говнокод #26957

    +2

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    Definition read_t key cont : Thread :=
          call tx_context <- get_tx_context;
          call cell <- get_cell key tx_context;
          match cell.(cell_write) with
          | Some v =>
              do _ <- log (read key v);
              cont v
          | None =>
              do v <- read_d key;
              let tx_context' := set tx_cells <[key := cell]> tx_context in
              do _ <- pd_set tx_context';
              do _ <- log (read key v);
              cont v
          end.

    Continuations are like violence, if they don't work then you're not using enough of them.

    Запостил: CHayT, 16 Сентября 2020

    Комментарии (33) RSS

    • SEO: продолжения это самый главный паттерн программирования. В языке нет I/O? Продолжения.
      Ответить
    • Ко-кок.
      Ответить
    • > продолжения

      В лучших традициях джаваскрипт фреймворков...

      do/call и стрелочка это эмуляция императивщины?
      Ответить
      • Как-то так, да. "do ret <- action" это Notation для конструктора типа trace event "процесс с пидом Pid выполнил сисколл action, и ему вернулося ret". Потом trace event'ы от разных процессов перемешиваются, и для каждой кобенации решается система уравнений. Eсли она не совместна, то значит кобенация невозможна (к примеру, два процесса входит в одну критическую секцию), если совместна, то она задаёт область пространства состояний системы, про которую можно что-то доказать.
        Ответить
        • Омг, т.е. там можно доказать отсутствие гонок?
          Ответить
          • Гонок — да, абсолютно, дедлоков — чуть сложнее. Этот метод больше про safety, а не liveness.
            Ответить
            • А отсутствие дедлоков вообще можно доказать? Это не эквивалентно проблеме останова?
              Ответить
              • Для любого частного случая можно что-то доказать (т.к. питуху требуется небольшой human guidance). В общем случае, нет, конечно.
                Ответить
                • Кстати, что ты там такое пилишь, что аж формальные пруфы нужны?
                  Ответить
                  • Движок кислотной БД. (Для будущего, где марсоходы будут бороздить просторы Большого театра)
                    Ответить
                    • Какой хардкор )))

                      А исполняться это будет через выгрузку в их верифицированный конпелятор си?
                      Ответить
                      • Выгружать во что-то функциональное придётся, ибо этот метод про I/O, а не про memory safety. (В теории и кучу, конечно, можно имитировать через I/O, но зачем)
                        Ответить
            • >safety, а не liveness
              Как в реальной жизни эти свойства доказываются? Твоя прога строит граф всех состояний системы? Бд это же асинхронная и недетерминированная система?
              Ответить
              • > Твоя прога строит граф всех состояний системы?

                Да. Все model-checker'ы так и работают. Но в моём случае состояние системы представлено не конкретно (как в "TLA+", "Promela", "Spin" и "Concuerror", например), а параметрически, в виде системы уравнений. Так веселее. Потом из доказательства про этот граф можно сделать тройку Хоара, а их уже можно как угодно кобенировать.

                > Бд это же асинхронная и недетерминированная система?

                Именно. Она использует сеть, которая пакеты теряет и т.д. Поэтому результат I/O действия определяется как множество возможных исходов. Опять-таки символьно.
                Ответить
                • >в виде системы уравнений
                  Переменные в ней это что?
                  Множество решений системы - множество состояний? Это сколько уравнений в системе получается?
                  Ответить
                  • > Переменные в ней это что?

                    Состояния частей системы. Если у тебя в стейте есть переменная, то состояние этой переменной. Если есть сеть, то список in-flight пакетов, и т.д.

                    > Множество решений системы - множество состояний?

                    Да.

                    > Это сколько уравнений в системе получается?

                    Экспоненциально много, иначе никак ^___~ Сейчас пилю оптимизацию про сокращение этого добра примерно на порядок, через знание о том, какие операции коммутируют.
                    Ответить
                    • А как выражены ребра графа?
                      Ответить
                      • В неоптимизированной референсной версии буквально так:
                        Inductive Interleaving : list TE -> list TE -> TraceEnsemble :=
                          | ilv_cons_l : forall te t1 t2 t,
                              Interleaving t1 t2 t ->
                              Interleaving (te :: t1) t2 (te :: t)
                          | ilv_cons_r : forall te t1 t2 t,
                              Interleaving t1 t2 t ->
                              Interleaving t1 (te :: t2) (te :: t)
                          | ilv_nil : Interleaving [] [] [].

                        В оптимизированной там формально верифицированный адок.
                        Ответить
                        • я тут пытаюсь себе представить что ты делаешь
                          у тебя есть какая-то модель из состояний и ограничений которая описывает систему, ты из нее строишь систему уравнений, решаешь и получаешь множество вершин графа. А откуда у тебя берется множество ребер?
                          Ответить
                          • Судя по тому, что Снаут выше писал - "трассировкой" всех вариантов поведения треда.
                            Ответить
                          • > А откуда у тебя берется множество ребер?

                            Из кода выше. "TE" (Trace Event) это и есть ребро графа. "list TE" — список сисколлов процесса (как если к нему strace'ом подрубиться). Он получается раскукоживанием кода из OP-поста. (На самом деле это и не код вовсе, а структура данных хитрая, которая кодирует все возможные поведения процесса).
                            Ответить
                            • Я понял что ничего не понял
                              Ты запускаешь бд, у тебя появляется высер из логов, ты его перемешиваешь и что-то доказываешь?
                              Ответить
                              • Я ничего не запускаю, а создаю структуру данных, описывающаю все возможные последовательности сисколлов (трейс), которые бд (вернее какая-то её подпрограмма) может вызвать. (См. OP-пост, это она). Затем кобенирую её с другими подпрограммами, с которыми она может устраивать гонки данных, и получаю экспоненциально большой набор трейсов уже от двух параллельных потоков. Затем я проверяю, возможен ли физически каждый трейс, если он возможен — что-то про него доказываю.
                                Ответить
                                • А откуда ты генерируешь эту структуру? Из исходного кода?
                                  Ответить
                                  • Просто DSL, который выглядит как "код".
                                    Ответить
                                  • Я её буквально пишу на говноDSL.
                                    Ответить
                                    • то есть ты пишешь и код может быть скомпилирован в исполняемый код или в структуру данных?
                                      Ответить
                                      • Вроде того. ГовноDSL на 90% состоит из "Gallina", которую можно превратить в ocaml, haskell и прочую питушню.
                                        Ответить
                                        • > Gallina

                                          Лоол. У них то питух то куритса.
                                          Ответить
                                        • А что будет по пифрормансу? Если скомпилировать что-то в высокоуровневый язык не получится что он скомилируется в ультра хуевый машинный код?
                                          Ответить
                                          • Это зависит всецело от того, в какой язык заэкстрактить. В Coq встроен транслятор, а не компилятор.
                                            Ответить

    Добавить комментарий