smt.html


<!doctype html>
<html lang="en" class="no-js">
  <head>
    
      <meta charset="utf-8">
      <meta name="viewport" content="width=device-width,initial-scale=1">
      
      
      <link rel="shortcut icon" href="assets/images/favicon.png">
      <meta name="generator" content="mkdocs-1.1.2, mkdocs-material-6.2.6">
    
    
        <title>#smt - PLComp</title>
      
    
      <link rel="stylesheet" href="assets/stylesheets/main.cb6bc1d0.min.css">
      
        
        <link rel="stylesheet" href="assets/stylesheets/palette.39b8e14a.min.css">
        
          
          <meta name="theme-color" content="#000000">
        
      
        <link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
        <link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Roboto:300,400,400i,700%7CRoboto+Mono&display=fallback">
        <style>body,input{font-family:"Roboto",-apple-system,BlinkMacSystemFont,Helvetica,Arial,sans-serif}code,kbd,pre{font-family:"Roboto Mono",SFMono-Regular,Consolas,Menlo,monospace}</style>
      
    
  </head>
  
  
    <body dir="ltr" data-md-color-scheme="" data-md-color-primary="black" data-md-color-accent="">
      
  
    <input class="md-toggle" data-md-toggle="drawer" type="checkbox" id="__drawer" autocomplete="off">
    <input class="md-toggle" data-md-toggle="search" type="checkbox" id="__search" autocomplete="off">
    <label class="md-overlay" for="__drawer"></label>
    <div data-md-component="skip">
      
        
        <a href="#02112020-peter-sovietov" class="md-skip">
          Skip to content
        </a>
      
    </div>
    <div data-md-component="announce">
      
    </div>
    
      
<header class="md-header" data-md-component="header">
  <nav class="md-header-nav md-grid" aria-label="Header">
    <a href="./index.html" title="PLComp" class="md-header-nav__button md-logo" aria-label="PLComp">
      
  
  <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M12 8a3 3 0 003-3 3 3 0 00-3-3 3 3 0 00-3 3 3 3 0 003 3m0 3.54C9.64 9.35 6.5 8 3 8v11c3.5 0 6.64 1.35 9 3.54 2.36-2.19 5.5-3.54 9-3.54V8c-3.5 0-6.64 1.35-9 3.54z"/></svg>

    </a>
    <label class="md-header-nav__button md-icon" for="__drawer">
      <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M3 6h18v2H3V6m0 5h18v2H3v-2m0 5h18v2H3v-2z"/></svg>
    </label>
    <div class="md-header-nav__title" data-md-component="header-title">
      <div class="md-header-nav__ellipsis">
        <div class="md-header-nav__topic">
          <span class="md-ellipsis">
            PLComp
          </span>
        </div>
        <div class="md-header-nav__topic">
          <span class="md-ellipsis">
            
              #smt
            
          </span>
        </div>
      </div>
    </div>
    
    
  </nav>
</header>
    
    <div class="md-container" data-md-component="container">
      
      
      <main class="md-main" data-md-component="main">
        <div class="md-main__inner md-grid">
          
            
              <div class="md-sidebar md-sidebar--primary" data-md-component="navigation" >
                <div class="md-sidebar__scrollwrap">
                  <div class="md-sidebar__inner">
                    

<nav class="md-nav md-nav--primary" aria-label="Navigation" data-md-level="0">
  <label class="md-nav__title" for="__drawer">
    <a href="./index.html" title="PLComp" class="md-nav__button md-logo" aria-label="PLComp">
      
  
  <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M12 8a3 3 0 003-3 3 3 0 00-3-3 3 3 0 00-3 3 3 3 0 003 3m0 3.54C9.64 9.35 6.5 8 3 8v11c3.5 0 6.64 1.35 9 3.54 2.36-2.19 5.5-3.54 9-3.54V8c-3.5 0-6.64 1.35-9 3.54z"/></svg>

    </a>
    PLComp
  </label>
  
  <ul class="md-nav__list" data-md-scrollfix>
    
      
    <li class="md-nav__item">
      <a href="index.html" class="md-nav__link">
        NEW
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="all.html" class="md-nav__link">
        ALL
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="analysis.html" class="md-nav__link">
        #analysis
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="registerallocation.html" class="md-nav__link">
        #registerallocation
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="history.html" class="md-nav__link">
        #history
      </a>
    </li>
  

    <li class="md-nav__item md-nav__item--active">
      
      <input class="md-nav__toggle md-toggle" data-md-toggle="toc" type="checkbox" id="__toc">
      
        
      <a href="smt.html" class="md-nav__link md-nav__link--active">
        #smt
      </a>
      
    </li>
  

    <li class="md-nav__item">
      <a href="parsing.html" class="md-nav__link">
        #parsing
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="conf.html" class="md-nav__link">
        #conf
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="synthesis.html" class="md-nav__link">
        #synthesis
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="jit.html" class="md-nav__link">
        #jit
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="ocaml.html" class="md-nav__link">
        #ocaml
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="optimization.html" class="md-nav__link">
        #optimization
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="garbagecollection.html" class="md-nav__link">
        #garbagecollection
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="dsl.html" class="md-nav__link">
        #dsl
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="semantics.html" class="md-nav__link">
        #semantics
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="ssa.html" class="md-nav__link">
        #ssa
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="compiler.html" class="md-nav__link">
        #compiler
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="lisp.html" class="md-nav__link">
        #lisp
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="modules.html" class="md-nav__link">
        #modules
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="llvm.html" class="md-nav__link">
        #llvm
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="stratego.html" class="md-nav__link">
        #stratego
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="linearscan.html" class="md-nav__link">
        #linearscan
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="bpf.html" class="md-nav__link">
        #bpf
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="lua.html" class="md-nav__link">
        #lua
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="datalog.html" class="md-nav__link">
        #datalog
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="machinelearning.html" class="md-nav__link">
        #machinelearning
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="gc.html" class="md-nav__link">
        #gc
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="fp.html" class="md-nav__link">
        #fp
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="haskell.html" class="md-nav__link">
        #haskell
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="rust.html" class="md-nav__link">
        #rust
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="education.html" class="md-nav__link">
        #education
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="leroy.html" class="md-nav__link">
        #leroy
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="classic.html" class="md-nav__link">
        #classic
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="sml.html" class="md-nav__link">
        #sml
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="constraintprogramming.html" class="md-nav__link">
        #constraintprogramming
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="unison.html" class="md-nav__link">
        #unison
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="registeralloc.html" class="md-nav__link">
        #registeralloc
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="instructionscheduling.html" class="md-nav__link">
        #instructionscheduling
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="separatecompilation.html" class="md-nav__link">
        #separatecompilation
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="stlc.html" class="md-nav__link">
        #stlc
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="linking.html" class="md-nav__link">
        #linking
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="scheme.html" class="md-nav__link">
        #scheme
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="trace.html" class="md-nav__link">
        #trace
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="jvm.html" class="md-nav__link">
        #jvm
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="graalvm.html" class="md-nav__link">
        #graalvm
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="bliss.html" class="md-nav__link">
        #bliss
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="lcc.html" class="md-nav__link">
        #lcc
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="fortran.html" class="md-nav__link">
        #fortran
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="ghc.html" class="md-nav__link">
        #ghc
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="grin.html" class="md-nav__link">
        #grin
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="survey.html" class="md-nav__link">
        #survey
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="ag.html" class="md-nav__link">
        #ag
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="types.html" class="md-nav__link">
        #types
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="spoofax.html" class="md-nav__link">
        #spoofax
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="gradual.html" class="md-nav__link">
        #gradual
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="art.html" class="md-nav__link">
        #art
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="android.html" class="md-nav__link">
        #android
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="dex.html" class="md-nav__link">
        #dex
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="isa.html" class="md-nav__link">
        #isa
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="verification.html" class="md-nav__link">
        #verification
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="vm.html" class="md-nav__link">
        #vm
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="ml.html" class="md-nav__link">
        #ml
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="transpilation.html" class="md-nav__link">
        #transpilation
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="solver.html" class="md-nav__link">
        #solver
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="vliw.html" class="md-nav__link">
        #vliw
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="superoptimizer.html" class="md-nav__link">
        #superoptimizer
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="autotuning.html" class="md-nav__link">
        #autotuning
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="editor.html" class="md-nav__link">
        #editor
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="emacs.html" class="md-nav__link">
        #emacs
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="smie.html" class="md-nav__link">
        #smie
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="indentation.html" class="md-nav__link">
        #indentation
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="nanopass.html" class="md-nav__link">
        #nanopass
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="langworkbench.html" class="md-nav__link">
        #langworkbench
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="cps.html" class="md-nav__link">
        #cps
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="pe.html" class="md-nav__link">
        #pe
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="python.html" class="md-nav__link">
        #python
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="cpp.html" class="md-nav__link">
        #cpp
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="comparison.html" class="md-nav__link">
        #comparison
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="implementation.html" class="md-nav__link">
        #implementation
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="scala.html" class="md-nav__link">
        #scala
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="metacompiler.html" class="md-nav__link">
        #metacompiler
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="interpreter.html" class="md-nav__link">
        #interpreter
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="multicore.html" class="md-nav__link">
        #multicore
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="synth.html" class="md-nav__link">
        #synth
      </a>
    </li>
  

    <li class="md-nav__item">
      <a href="codegen.html" class="md-nav__link">
        #codegen
      </a>
    </li>
  

  </ul>
</nav>
                  </div>
                </div>
              </div>
            
            
              <div class="md-sidebar md-sidebar--secondary" data-md-component="toc" >
                <div class="md-sidebar__scrollwrap">
                  <div class="md-sidebar__inner">
                    
<nav class="md-nav md-nav--secondary" aria-label="Table of contents">
  
  
</nav>
                  </div>
                </div>
              </div>
            
          
          <div class="md-content">
            <article class="md-content__inner md-typeset">
              
                
                <h1 id="02112020-peter-sovietov"><span style="font-weight:normal;font-style:italic;font-size:medium">02/11/2020, Peter Sovietov</span><a class="headerlink" href="#02112020-peter-sovietov" title="Permanent link">&para;</a></h1>
<p>Очередная работа от John Regehr со товарищи на тему супероптимизации.</p>
<p><strong>Dataflow-based Pruning for Speeding up Superoptimization </strong>
<a href="https://www.cs.utah.edu/~regehr/dataflow-pruning.pdf">https://www.cs.utah.edu/~regehr/dataflow-pruning.pdf</a></p>
<p>Заметно, как первая эйфория от полностью автоматического применения SMT-решателя и метода CEGIS уходит. Оказывается, для задач реалистичных размерностей все равно приходится придумывать если не полностью собственную процедуру поиска с учетом эвристик из предметной области, то хотя бы ее элементы &ndash; иначе SMT-решателю справиться будет тяжело. </p>
<p>Ключевая идея авторов &ndash; прежде чем передавать на вход SMT-решателю очередную программу-кандидат из пространства поиска, полезно эту недооформленную программу (описывающую целое семейство конкретных программ) проверить на соответствие спецификации с помощью абстрактной интерпретации (анализ потоков данных на предмет known bits, int. ranges и так далее). В том числе, на конкретных тестовых входах.</p>
<p>В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.</p>
<p><a href="analysis.html">#analysis</a> <a href="synthesis.html">#synthesis</a> <a href="smt.html">#smt</a></p>
<hr />
<h1 id="16102020-peter-sovietov"><span style="font-weight:normal;font-style:italic;font-size:medium">16/10/2020, Peter Sovietov</span><a class="headerlink" href="#16102020-peter-sovietov" title="Permanent link">&para;</a></h1>
<p>Пособие по реализации проверки для refinement-типов. В духе разработки компиляторов на основе техники nanopass. Предикаты проверяются с помощью SMT-решателя Z3.</p>
<p><strong>Refinement Types: A Tutorial </strong>
<a href="https://arxiv.org/abs/2010.07763">https://arxiv.org/abs/2010.07763</a>
<a href="https://github.com/ranjitjhala/sprite-lang">https://github.com/ranjitjhala/sprite-lang</a></p>
<p><a href="analysis.html">#analysis</a> <a href="smt.html">#smt</a></p>
<hr />
<h1 id="08082020-peter-sovietov"><span style="font-weight:normal;font-style:italic;font-size:medium">08/08/2020, Peter Sovietov</span><a class="headerlink" href="#08082020-peter-sovietov" title="Permanent link">&para;</a></h1>
<p>Formulog &ndash; выразительный DSL для задач статического анализа.
Основан на Datalog и ML, реализация использует SMT-решатель.</p>
<p><strong>Formulog: ML + Datalog + SMT </strong>
<a href="http://www.weaselhat.com/2020/08/07/formulog-ml-datalog-smt/">http://www.weaselhat.com/2020/08/07/formulog-ml-datalog-smt/</a></p>
<p><a href="datalog.html">#datalog</a> <a href="analysis.html">#analysis</a> <a href="smt.html">#smt</a></p>
<hr />
<h1 id="17062020-peter-sovietov"><span style="font-weight:normal;font-style:italic;font-size:medium">17/06/2020, Peter Sovietov</span><a class="headerlink" href="#17062020-peter-sovietov" title="Permanent link">&para;</a></h1>
<p>В рамках PLDI Alex Aiken (известный многим по курсам компиляторостроения) рассказал о проекте TASO &ndash; это автоматический синтез графовых оптимизирующих преобразований для нейросетевых фреймворков. Перечисляются все графы-шаблоны нейросетевых операций до фиксированного размера, между графами устанавливается соответствие с помощью Z3, преобразования графов программ происходят с помощью механизма отката и стоимостной модели. В целом, рассказ повторяет эту статью:</p>
<p><strong>TASO: Optimizing Deep Learning Computation with Automatic Generation of Graph Substitutions </strong>
<a href="https://cs.stanford.edu/~padon/taso-sosp19.pdf">https://cs.stanford.edu/~padon/taso-sosp19.pdf</a></p>
<p><a href="synthesis.html">#synthesis</a> <a href="smt.html">#smt</a></p>
<hr />
<h1 id="05062020-peter-sovietov"><span style="font-weight:normal;font-style:italic;font-size:medium">05/06/2020, Peter Sovietov</span><a class="headerlink" href="#05062020-peter-sovietov" title="Permanent link">&para;</a></h1>
<p>Доклад <strong>Improving Compiler Construction Using Formal Methods</strong> (Jubi Taneja)
Обзор работ по теме использования супероптимизатора Souper в различных фазах компиляции (статический анализ, автоматизация создания правил локальной оптимизации).
<a href="https://www.youtube.com/watch?v=de8Ak0nY1hA">https://www.youtube.com/watch?v=de8Ak0nY1hA</a></p>
<p><a href="superoptimizer.html">#superoptimizer</a> <a href="smt.html">#smt</a></p>
<hr />
<h1 id="27052020-peter-sovietov"><span style="font-weight:normal;font-style:italic;font-size:medium">27/05/2020, Peter Sovietov</span><a class="headerlink" href="#27052020-peter-sovietov" title="Permanent link">&para;</a></h1>
<p>Очень доходчивый и практико-ориентированный разбор одной из ключевых статей в области супероптимизации на основе метода CEGIS. Автор даже не поленился расшифровать формулы из статьи для тех, кто сторонится математической нотации.
<strong>Synthesizing Loop-Free Programs with Rust and Z3 </strong>
<a href="https://fitzgeraldnick.com/2020/01/13/synthesizing-loop-free-programs.html">https://fitzgeraldnick.com/2020/01/13/synthesizing-loop-free-programs.html</a></p>
<p><a href="synthesis.html">#synthesis</a> <a href="smt.html">#smt</a></p>
                
              
            </article>
          </div>
        </div>
      </main>
      
        
<footer class="md-footer">
  
    <div class="md-footer-nav">
      <nav class="md-footer-nav__inner md-grid" aria-label="Footer">
        
          <a href="history.html" class="md-footer-nav__link md-footer-nav__link--prev" rel="prev">
            <div class="md-footer-nav__button md-icon">
              <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M20 11v2H8l5.5 5.5-1.42 1.42L4.16 12l7.92-7.92L13.5 5.5 8 11h12z"/></svg>
            </div>
            <div class="md-footer-nav__title">
              <div class="md-ellipsis">
                <span class="md-footer-nav__direction">
                  Previous
                </span>
                #history
              </div>
            </div>
          </a>
        
        
          <a href="parsing.html" class="md-footer-nav__link md-footer-nav__link--next" rel="next">
            <div class="md-footer-nav__title">
              <div class="md-ellipsis">
                <span class="md-footer-nav__direction">
                  Next
                </span>
                #parsing
              </div>
            </div>
            <div class="md-footer-nav__button md-icon">
              <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M4 11v2h12l-5.5 5.5 1.42 1.42L19.84 12l-7.92-7.92L10.5 5.5 16 11H4z"/></svg>
            </div>
          </a>
        
      </nav>
    </div>
  
  <div class="md-footer-meta md-typeset">
    <div class="md-footer-meta__inner md-grid">
      <div class="md-footer-copyright">
        
        Made with
        <a href="https://squidfunk.github.io/mkdocs-material/" target="_blank" rel="noopener">
          Material for MkDocs
        </a>
      </div>
      
    </div>
  </div>
</footer>
      
    </div>
    
      <script src="assets/javascripts/vendor.53cc9318.min.js"></script>
      <script src="assets/javascripts/bundle.e9c9f54f.min.js"></script><script id="__lang" type="application/json">{"clipboard.copy": "Copy to clipboard", "clipboard.copied": "Copied to clipboard", "search.config.lang": "en", "search.config.pipeline": "trimmer, stopWordFilter", "search.config.separator": "[\\s\\-]+", "search.placeholder": "Search", "search.result.placeholder": "Type to start searching", "search.result.none": "No matching documents", "search.result.one": "1 matching document", "search.result.other": "# matching documents", "search.result.more.one": "1 more on this page", "search.result.more.other": "# more on this page", "search.result.term.missing": "Missing"}</script>
      
      <script>
        app = initialize({
          base: ".",
          features: [],
          search: Object.assign({
            worker: "assets/javascripts/worker/search.9c0e82ba.min.js"
          }, typeof search !== "undefined" && search)
        })
      </script>
      
    
  </body>
</html>