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

    • ava CHayT 01.11.2021 01:46 # +1

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

      • ava CHayT 01.11.2021 02:26 # +1

        А разгадка в бектрекинге: тактика должна размотать второй процесс, применяя третий конструктор до тех пор, пока либо не наткнётся на некоммутирующий вызов в первом процессе, тогда она может применить второй конструктор и вернуть полученный трейс. Либо же она доходит до конца второго треда, понимает, что собрать правильный трейс ей не удастся, и откатывает весь этот путь назад.
        Ответить

        • ava guest6 01.11.2021 02:32 # +1

          Какой НКА, почти как в рагулярках
          Ответить

        • ava CHayT 01.11.2021 13:57 # 0

          P.S. А всё потому, что мне было лень менять одно из ключевых определений, которое изначально было не очень удобным. Если бы пид процессов изначально жил отдельно от определения ио-псов, не пришлось бы городить этот хак. Такая вот техническая долговая яма вышла.
          Ответить

    • ava CHayT 01.11.2021 01:49 # +1

      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.
      Ответить

      • ava j123123 01.11.2021 06:03 # +2

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

        И допустим в эту хуйню передается два нуля как аргумент. Что она вернет? По первому совпадению, т.е. 0? Или это вообще не "скомпилируется"?
        Ответить

        • ava CHayT 01.11.2021 11:37 # +1

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

          • ava nemyx 17.03.2024 22:15 # 0

            А в Curry и Ltac как?
            Ответить

            • ava guest6 17.03.2024 22:23 # 0

              ну судя по наличию там бектрекинга, он работает до самого "полного" совпадения, как маленькая жадная регулярка

              Это знечит, что опотный программист может написать такой паттерн-матчинг, который за экспоненциальное время будет работать, и повесит тебе машину нахуй
              Ответить

    • ava digitalEugene 01.11.2021 08:55 # −1

      потому что ты долбоёб блять
      Ответить

      • ava CHayT 01.11.2021 12:05 # 0

        Ругаешься как румяный гимназист.
        Ответить

        • ava digitalEugene 01.11.2021 15:49 # 0

          это мемасик такой.
          Ответить

          • ava bormand 01.11.2021 16:21 # 0

            За такой мемасик в реальчике дают по ебальцу.
            Ответить

            • ava Desktop 01.11.2021 16:33 # 0

              http://randomoverload.org/wp-content/uploads/2013/02/7342funny-T-rex-small-hands.jpg
              Ответить

            • ava guest6 17.03.2024 22:24 # 0

              >в реальчике дают по ебальцу.

              так вижу
              https://youtu.be/rX8j3TAG1qY?t=66
              Ответить

              • ava Desktop 17.03.2024 22:29 # 0

                могли бы по жопе, но жопа под заshitой, а потому приходится по ебальцу
                Ответить

          • ava CHayT 01.11.2021 16:41 # +1

            Шитпостишь как престарелая библиотекарша в одноклассниках.
            Ответить

    • ava CHayT 09.11.2021 21:11 # 0

      Вот так, нять, надо коммутирующие айопсы чистить.
      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.
      Ответить

      • ava CHayT 09.11.2021 21:12 # 0 

        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!
        Ответить

        • ava CHayT 09.11.2021 21:17 # 0

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

      • ava bormand 09.11.2021 23:53 # 0

        > g g' g'0

        Сразу видно ма-те-ма-ти-чес-кую школу.
        Ответить

        • ava CHayT 10.11.2021 00:10 # 0

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

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