Ivy was introduced in a 2016 PLDI paper “Ivy: Safety Verification by Interactive Generalization“. Ivy helps proof engineers find inductive invariants for proving code safety properties. One of the authors published helpful slides. The code is open sourced under the GPL, with an archived version on Microsoft’s Github, which now directs interested parties to kenmcmil/ivy. […]
Author Archive: yonch
SCIP on MacOS: how to install the MIP optimizer
SCIP is an open source optimizer that solves Mixed Integer Programs (MIP). Since version 8.0.3 it is released under the Apache 2.0 license, making it available to a large variety of projects (a huge “thank you” to the SCIP team for this license choice!). I have experimented with using SCIP via the recently released version […]
How to Accelerate Slow Rust CI/CD Builds on Google Cloud Build
Rust’s cargo provides powerful dependency management, allowing projects to easily leverage community developed libraries to build new functionality. Cargo’s local cache speeds up local cargo builds when build configuration does not change: dependencies only need to be built once, so subsequent builds are faster. However, when running plain cargo in build containers on CI platforms, […]
DNS Resolver Libraries
We had an application that required parsing received DNS response packets for queries made by other applications. DNS packet structure is a 12-byte header, followed by question entries in the question format, followed by entries in answer, authoritative, and additional sections in the resource record (RR) format. The header specifies the number of entries in each of […]
Linux TCP congestion control internals
Linux has a pluggable TCP congestion control architecture: the IPv4 and IPv6 implementations both call a set of functions that implement congestion control. The congestion-control algorithm can be changed system-wide for new connections, or set for individual sockets using setsockopt (more info here). Here, we look at how the TCP implementation interacts with the congestion […]
Preparing a private git repository for public release
A git project that is open-sourced could require some manipulation before it is ready for release such as changing the directory structure and cleaning out irrelevant files. When the repository contains a single sub-directory with content to release (and only such content), there are methods to split a git repository. This post covers techniques for […]
Recovering Eclipse workspaces from CDT errors
I use unison to synchronize work environments between different workstations (more convenient than rsync IMO), and include the eclipse workspace in the synchronized directory. The problem is sometimes, if the remote eclipse is running, sync will corrupt some workspace state that prevents Eclipse from running. This happens to me every 2-3 months. Eclipse displays an […]
Creating an LTTng tracepoint file
LTTng is a framework to collect kernel tracepoint logs with low overhead (see 5.5 in Desnoyers’ thesis for eval). Instrumenting the kernel is done in two parts: adding a kernel tracepoint, and writing the LTTng adaptation layer. The process is documented in a section of the LTTng docs, however there are a few points that […]
Linux kernel 3.x call-graphs with ncc-2.8
ncc is a compiler, built specifically to extracts call-graph information from source code. One strong feature is analysis of function pointers. Call graphs can help explore and learn large code bases, which makes it especially useful for the Linux kernel. ncc comes with documentation on extracting call-graphs from 2.6 kernels, apparently tested circa 2008. We […]
Creating call-graphs to explore the Linux kernel with CodeViz
This article uses CodeViz, which downloads gcc 4.6.2 to compile the kernel while extracting code information. Other posts explore other techniques. Making codeviz and gcc The makefile calls the script “compilers/install_gcc-4.6.2.sh” to compile the patched gcc. There might be a few changes to that script in order to get everything working. Thanks to Stephan Friedl’s […]