I’m serving on the program committee for the 2018 Workshop on Principles and Practice of Consistency for Distributed Data, co-located with EuroSys ‘18 in Porto, Portugal. This will be my second time on the PC of PaPoC, a workshop that I like a lot.
Recently I remarked on Twitter, “I should donate to archive.org more. They’re how I know that large parts of my own past actually happened.” By “archive.org” I meant the Internet Archive, the organization that runs the Wayback Machine and many other projects. Here are three stories from 2017 about what I mean by that remark.
Something I really like about my blogging setup here on composition.al is that my posts are just plain old version-controlled text files. Years ago, Dave Herman remarked on how nice it is to be able to blog using one’s text editor, and I feel the same way. But there’s so much more to it than just being able to write my posts in my editor of choice. For me, the more important thing is that I can make use of the vast number of tools out there for manipulating text, including and especially versioned text. Because of that, I don’t have to wait for my blogging framework to implement this or that feature. I can just use tools that already exist.
This year, as I’ve started to dive into neural network verification, I’ve had the chance to learn a little about how SMT solvers are implemented. One thing I learned that surprised me is that under the hood, many state-of-the-art SMT solvers use the simplex algorithm to solve satisfiability problems.
Halide is a newish domain-specific language for writing high-performance image processing pipelines, originally created by a group of researchers at MIT and Adobe and now used in lots of places. Although the original paper on Halide appeared at SIGGRAPH 2012, I like the PLDI 2013 paper better as an introduction to this line of work.
Halide is really two languages: one for expressing the algorithm you want to compute, and one for expressing how you want that computation to be scheduled. In fact, the key idea of Halide is this notion of separating algorithm from schedule.