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

    +1

    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
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    22. 22
    23. 23
    24. 24
    25. 25
    26. 26
    27. 27
    28. 28
    (** Set of all possible interleaving of two traces is a trace
      ensemble. As we later prove in [interleaving_to_permutation], this
      definition is dual to [Permutation]. *)
      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 [] [] [].
    
    Попытка оптимизации:
    
      (* Left-biased version of [Interleaving] that doesn't make
      distinction between schedulings of commuting elements: *)
      Inductive UniqueInterleaving : list TE -> list TE -> TraceEnsemble :=
      | uilv_cons_l : forall l t1 t2 t,
          UniqueInterleaving t1 t2 t ->
          UniqueInterleaving (l :: t1) t2 (l :: t)
      | uilv_cons_r1 : forall l r t1 t2 t,
          ~trace_elems_commute l r ->
          UniqueInterleaving (l :: t1) t2 (l :: t) ->
          UniqueInterleaving (l :: t1) (r :: t2) (r :: l :: t)
      | uilv_cons_r2 : forall r1 r2 t1 t2 t,
          UniqueInterleaving t1 (r1 :: t2) (r1 :: t) ->
          UniqueInterleaving t1 (r2 :: r1 :: t2) (r2 :: r1 :: t)
      | uilv_nil : forall t, UniqueInterleaving [] t t.

    Сложный говнокод. Почему вторая "оптимизированная" версия работает хуже первой?

    Запостил: CHayT, 01 Ноября 2021

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

    • SEO: для того, чтобы доказать что-то про недетерминированную систему (любая система, которая совершает I/O такой является) мы используем трейсы. Если эта система ещё и параллельная/распределённая до кучи, то мы эти трейсы должны особым образом перемешать (см. первый пример). Количество таких перемешиваний растёт примерно по экспоненте, и это плохо. Однако, некоторые операции коммутируют, и это хорошо. Мы эти коммутирующие операции можем из рассмотрения выкинуть, и степень экспоненты уменьшается (см. второе пиздец изящное определение). Оно формально правильно, Снаутяша это доказала. Количество трейсов реально уменьшается. Однако, тактика, которая эти трейсы разворечивает имеет такую же асимтотику, что и тупая тактика, но с большим (!) множителем. Вопрос к залу, как так вышло.
      Ответить
      • А разгадка в бектрекинге: тактика должна размотать второй процесс, применяя третий конструктор до тех пор, пока либо не наткнётся на некоммутирующий вызов в первом процессе, тогда она может применить второй конструктор и вернуть полученный трейс. Либо же она доходит до конца второго треда, понимает, что собрать правильный трейс ей не удастся, и откатывает весь этот путь назад.
        Ответить
        • Какой НКА, почти как в рагулярках
          Ответить
        • P.S. А всё потому, что мне было лень менять одно из ключевых определений, которое изначально было не очень удобным. Если бы пид процессов изначально жил отдельно от определения ио-псов, не пришлось бы городить этот хак. Такая вот техническая долговая яма вышла.
          Ответить
    • P.S. Дампик Точная формула сложности доказательства, если кому интересно:

      Fixpoint num_interleavings (a b : nat) : nat :=
          match a, b with
          | 0, _   => 1
          | _, 0   => 1
          | _, S b => fold_left (fun acc i => acc + (num_interleavings i b)) (seq 0 (S a)) 0
          end.
      Ответить
      • Мне вообще не нравится эта ML-нутая хрень с матчингом. Если смотришь на это в первый раз, тут есть явные неоднозначности
        Вот допустим у меня есть такая хрень
        Fixpoint someshit (a b : nat) : nat :=
            match a, b with
            | 0, _   => 0
            | _, 0   => 1
            | _, _   => 2
            end.

        И допустим в эту хуйню передается два нуля как аргумент. Что она вернет? По первому совпадению, т.е. 0? Или это вообще не "скомпилируется"?
        Ответить
        • Во всех ФП языках, кроме логических с бэктрекингом (Curry, Ltac), паттерн-матчинг работает сверху вниз до первого совпадения. Так что жалоба в духе джавамэнов, что "в сишке нужно free делать".
          Ответить
          • А в Curry и Ltac как?
            Ответить
            • ну судя по наличию там бектрекинга, он работает до самого "полного" совпадения, как маленькая жадная регулярка

              Это знечит, что опотный программист может написать такой паттерн-матчинг, который за экспоненциальное время будет работать, и повесит тебе машину нахуй
              Ответить
    • потому что ты долбоёб блять
      Ответить
      • Ругаешься как румяный гимназист.
        Ответить
        • это мемасик такой.
          Ответить
          • За такой мемасик в реальчике дают по ебальцу.
            Ответить
            • http://randomoverload.org/wp-content/uploads/2013/02/7342funny-T-rex-small-hands.jpg
              Ответить
            • >в реальчике дают по ебальцу.

              так вижу
              https://youtu.be/rX8j3TAG1qY?t=66
              Ответить
              • могли бы по жопе, но жопа под заshitой, а потому приходится по ебальцу
                Ответить
          • Шитпостишь как престарелая библиотекарша в одноклассниках.
            Ответить
    • Вот так, нять, надо коммутирующие айопсы чистить.
      Inductive GenEnsembleOpt (g : Gen) : @TraceEnsemble TE :=
        | og_ens_nil :
            g  ~~>x ->
            GenEnsembleOpt g []
        | og_ens_first : forall g' te,
            g  ~~> g' & te ->
            g' ~~>x ->
            GenEnsembleOpt g [te]
        | og_ens_cons : forall g' te te' t,
            g ~~> g' & te ->
            can_follow te te' ->
            GenEnsembleOpt g' (te' :: t) ->
            GenEnsembleOpt g (te :: te' :: t).
      
        Fixpoint gen_ens_opt_add g g' te te' t (Hte : g ~~> g' & te)
                 (Ht : GenEnsembleOpt g' (te' :: t))
                 (HG : generator_events_commute Gen)
                 (Hfoll : ~ can_follow te te') {struct Ht} :
          exists t' : list TE, GenEnsembleOpt g (te' :: t') /\ Permutation events_commute (te :: te' :: t) (te' :: t').
        Proof with auto with slot.
          destruct te as [pid evt]. destruct te' as [pid' evt'].
          firstorder. apply NNPP in H0. rename H0 into Hcomm.
          assert (Hpids : pid <> pid') by lia.
          inversion Ht; subst; clear Ht.
          - exists [pid @ evt]. split.
            + specialize (HG g g' g'0 (pid @ evt) (pid' @ evt') Hpids).
              destruct HG as [g_ [Hg_ Hg_']]...
              constructor 3 with g_...
              * left. lia.
              * constructor 2 with g'0...
            + constructor 3...
          - specialize (HG g g' g'0 (pid @ evt) (pid' @ evt') Hpids) as Hgen_comm.
            destruct Hgen_comm as [g_ [Hg_ Hg_']]...
            destruct (classic (can_follow (pid @ evt) te')) as [Hfoll' | Hfoll'].
            + exists (pid @ evt :: te' :: t0). split.
              * constructor 3 with g_...
                -- left. lia.
                -- constructor 3 with g'0...
              * constructor 3...
            + specialize (gen_ens_opt_add g_ g'0 (pid @ evt) te' t0) as IH. clear gen_ens_opt_add.
              destruct IH as [t' [Ht' Hperm']]...
              exists (te' :: t'). split.
              * constructor 3 with g_...
              * sauto.
        Qed.
      Ответить
      • Fixpoint gen_ens_opt (g : Gen) (t : list TE) (Ht : GenEnsemble g t)
                   (HG : generator_events_commute Gen)
                   {struct Ht} :
            exists t' : list TE, GenEnsembleOpt g t' /\ Permutation events_commute t t'.
          Proof with auto with slot.
            destruct Ht as [Hnil | g' te t Hte Ht].
            - exists []. split; now constructor.
            - apply gen_ens_opt in Ht. destruct Ht as [t' [Ht' Hperm]]; clear gen_ens_opt.
              destruct t' as [ | te' t'].
              + exists [te].
                apply perm_empty in Hperm; subst.
                split.
                * inversion Ht'. constructor 2 with g'...
                * repeat constructor.
              + destruct (classic (can_follow te te')).
                * exists (te :: te' :: t'). split.
                  -- constructor 3 with g'...
                  -- now constructor.
                * eapply gen_ens_opt_add in Ht'; eauto.
                  destruct Ht' as [t'' [Ht'' Hperm'']].
                  exists (te' :: t''). split.
                  -- assumption.
                  -- apply perm_trans with (te :: te' :: t')...
              + assumption.
          Qed.
        
          Theorem optimize_gen_p g
            (HG : generator_events_commute Gen) :
            sufficient_replacement_p (GenEnsemble g) (GenEnsembleOpt g).
          Proof.
            intros t Ht.
            now apply gen_ens_opt.
          Qed.
        
          Theorem optimize_gen (g : Gen) P Q (HG : generator_events_commute Gen) :
            -{{ P }} GenEnsembleOpt g {{ Q }} ->
            -{{ P }} GenEnsemble g {{ Q }}.
          Proof.
            now apply ht_sufficient_replacement, comm_perm_sufficient_replacement, optimize_gen_p.
          Qed.

        sauto, sauto, sauto, sauto! firstorder. sauto!
        Ответить
        • P.S. induction для слабаков, мы — девочки-волшебницы, мы делаем индукцию fixpoint'ами.
          Ответить
      • > g g' g'0

        Сразу видно ма-те-ма-ти-чес-кую школу.
        Ответить
        • Лень было переименовывать что там inversion нагенерила. Поэтому я за ``Coq'': между Proof и Qed может быть любая дикая говнота, написаная левой лапкой, лишь бы coqchk её жрал.
          Ответить

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