My Talk

My talk was about egglog https://www.philipzucker.com/egglog/, the egraphs based datalog.

It went very nice.

Recollections

Went over on saturday, visited Sarah and Bron. Got to see the house. Very neat. There is a lot to say for California. Rode the surfliner train up from San Diego.

The conference was fun. I was pleasantly surprised by how many people has seen my tinkerings online. The EGRAPHS woskhop was of course a highlight. I decided fairly last minute to go for in the window ASCII thing instead of just slamming out a Beamer, which I think came off really nicely. I actually loved only having 15 minutes. It takes a lot of stress off the preparation. I could talk about 15 minutes about anything and it really let me just focus on the essential points.

I was in a hotel a good mile or two from the main venue, which I actually kind of liked for the morning walk. God California is awesome. I just love good weather.

The whole UW crew was astonishingly welcoming of me, which I really appreciate. It was a little spooky lone wolfin’ it. I still feel a bit of an outsider in the PL world despite it being my main jam for 5 years or so now.

Had some great conversations with Eddie Jones and Stephen Ramsey. An interesting Saturday hanging out and killing time before flights with Oliver and Matt Flatt, two fellas who know things. I asked about the idea of SMTpp in Racket. Matt said a good fit. That seems likely, but what else was he gonna say :) ?

The tacos were incredible.

Notes

Checked C https://github.com/URSEC/checkedc-tutorial-pldi22

new PL - rust. but we gotta get that legacry C code

convert to checked-C

out of bound -

temporal memory safeyy - usae aftr free double free invalid free

_Ptr<> - no pointer artihemtic or subscript operatro _Array_ptr _Nt_array_ptr

null pointer check inseted by compiler

_array_ptr<> p : count(bounds_exp) = …; gives bound. Removes dynamic check if it can

upper and lower bounds _Array_ptr p1 : bounds(p0, p0 + BUF_LEN/2)

Nt_array_ptr pointing to null terminated _Nt_array_ptr p0 : count(5) = "12345";

automaitc bounds widening if (*p == ‘a’) { /// now I know p[0] wasn’t null }

checked regions _Checked only chfked pointers allowed. “a formal model of checked C”

_unchecked. force compiler to omit checking similar to rust undage

#pargama CHECKED_SSCOPE on all code is checked

Bounds safe interface

itype interoperation type. Can be checkd or unchecked char *dst : itype(_Array_ptr)

dynamic bound check dynamics_bounds_cast()

itype “is a forall”?

Question: Can I use any C compiler?

3C whle program static analyis infer bounds interactive annotation of C programs OOPSLA ‘22 typ3c . Ccured Cqual. chk wild pointer. how is it used ptr, arr ntarr root cause analysis modular checked pointer identificatin bound3c inferring bounds correlation analysis - locksmith finding daya races

ptr and array_ptr have subtyping relationship

clang tools https://clang.llvm.org/extra/index.html

adds intializers

require annotations? Are those dynamic checks? _assume_bounds_cast itype are not safe

snprintf

each commit of veriftpd shows change they made httpd libjpeg

3c root cause –itypes-for-extern

github / kokke. tiny C versions for embedded cstl corejson freestor

safety of unoxboed code RLbox - unsafe code and sandbox it.

Futhark

alive2

regehr formal semantics of llvm https://github.com/regehr/pldi22-llvm-tutorial

2 functions src and tgt tries to prove tgt is optimizaed version of source

mul –> shl

dsl for all bitwidthcs in alive

bitwdith indepndent proofs

How does it work? Could it be llvm independent?

counterexample simplification loop

rust has unchecked usigned

outlining? as compared to inlining. for code size. … huh

more rfefined undefined behavior

making partial things total Hmm. undef - adversarial vs optimization.

each ssa use of undef can return different values

poison is contagious. supports speculation it lives outside the values vector poison 2017 paper

Make sure my thing works offline

compiler to llvm

noundef

superoptimization Minotaur

divide by zero

(1/x) = 3 refines 1/x = undef.

if (x = 0) then 1/x = undef else 1/x=1/x egraph containment?

We’d need to case on x… hmmm.

x = 0 xor neq(x,0) neq(eq(x,0),neq(x,0)). Hmm, the group thing? We can throw this in the bool != bool eq(x,0) != neq(x,0)

eq(x,0) = eq() This is stupid. Do the undef splitting at meta level?

EGRAPHS2022

Thomas koehler - sketch guided equality satruations

matrix multiplciation blocking permutation unrolling change data layout parallelism RISE split-join transpose around map amp

shape of optimized program. sketch term with holes? an ematching pattern

A = Scaling

It’s almost the same problem as the categroy theory problem. rewriting stategies

backwards wiritng the sketches? Meet halfway rght?

Ian Briggs -

range reduction generate identities enode extraciton

extract every enode in eclass.
what was that about f(?x)? This seems key and I didn’t get it
it does feel eggloggy. directly manpulation
symettries - group union find

s(f(t(x))) transformations discover expressions that contain f?

Yihong

congruence add(a,b) -> c Great talk. Too adrenalined up to listen too closely, but it seemed like an excellent presentiation of the relational <-> egraph relationsip

Nadia

Tree automata?

egraphs equality constrained tree automata

compactly reprsetned constrained term spaces

dnumerate the dpace. tyoe druven program synthesis hoogle+

set of terms not equivalent. Just two things. Sets of terms add constraints at enodes? “reverse de bruijn notation”

any(x) holding all choices. any(1) = any(2)

Any = Var in reverse de bruijn You can encode SAT?

Remy

VSA tree automata

tactic for proof assitant

instantiate from context. 1 -> (- a a)

Rewrite rules can’t go both ways because of 1 = sub(a,a) :- term(a).

json rewrites work on logical equivalences. Equivalence is equality on bools or prop.

Kiran

suslik CHR rules concrete union find proof repair of List.iter heap manipulating programs cfml

Rebecca Swaords - egraphs in python

python ast rewriting https://github.com/riswords/quiche

Remy take II

egraph = DFTA eclass = state enode connects class to children - a trasnition conrects instates to outstate root class = final state accepts terms

String automata as special case. Linear egraphs.

https://github.com/ondrik/libvata monadic second order logic finite word automata

https://remy.wang/reports/dfta.pdf

ILP huh.

Eecenur Ustun - opsitimization integer onf fpg

Wasm

Haas bringing the web up to speed with webassembly

github.com/lifting-bits/eqsat

Sam coward - abstract intereptation

Colored Egraphs

proof search apply partial functions

multiset semantics - terminatine under set semantics

PLDI actually

hardneed binary parsers

cycleq cyclist

hipspec and zebo https://github.com/danr/hipspec “subst rule is special cut

ocamlfdo- https://github.com/gretay-js/ocamlfdo

ple niki vazou new paper

exo compilation

theory exploration

Semgus Sygus - applications of egraphs?

Parallelism rewrites using egraphs.

Sara Archour http://people.csail.mit.edu/sachour/#research cool analog computer stuff

FPL - fast small ILPs for compilers

RLibm

KMT - Green

La coccine joshua tree restaurant

Denis Xaiver- mlcfg. Creusot, stackify algorithm.

Paul Tarau - big tree

Kiran - ground your chr rules. Much faster.

Nominal sets are kind of finite?

Diffing of egraphs