Куча говна / Говнокод #26957 Ссылка на оригинал

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  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 CHayT, (Updated )

Комментарии (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 на 90% состоит из "Gallina", которую можно превратить в ocaml, haskell и прочую питушню.
                                      Ответить
                                      • А что будет по пифрормансу? Если скомпилировать что-то в высокоуровневый язык не получится что он скомилируется в ультра хуевый машинный код?
                                        Ответить
                                        • Это зависит всецело от того, в какой язык заэкстрактить. В Coq встроен транслятор, а не компилятор.
                                          Ответить

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

Помни, guest, за тобой могут следить!

    А не использовать ли нам bbcode?


    8