The first day of the conference was unexpected. The reports that I considered uninteresting for me turned out to be quite attractive, and vice versa: those that I chose for myself that day were not so brilliant.

The first big topic was machine learning. I am not familiar with it, but the reports seemed me quite interesting.

In the field of Machine Learning, two whole papers were devoted to optimizing data parallelism.

The first speaker said that often naive parallelization according to the data is not a tangible gain, because the exchange of messages between the individual computing units leads to sequential execution of the code.

The speaker suggested using a pipeline with a grouping of tasks according to the time of their execution. He also noted that some effort was necessary to be sure that all nodes deal with the same version of weights.

The second speaker talked about a universal scheduler for popular DNN frameworks. This scheduler, unlike its predecessors, takes into account the dependencies between tasks and minimizes the time spent on communication and waiting for the result.

The third report was devoted to the application of the erasure coding idea to restore classification results in cloud neural network services. A neural network was used, which is capable of producing a combined probability vector as the output for the sum of several inputs. From this vector it is possible to restore approximate classification results for each of the inputs, even if one of them is not available for any reason.

The fourth report described TASO - a special software tool that optimizes graphs of operations in neural networks and verifies correctness of such optimisations using automated theorem provers.

#SOSP19

Most interesting report in the second session was about an architecture of a secure transaction approval device. The researchers decided to use a separate RISC-V based SoC to isolate execution of transaction approval apps from OS that operates with secure storage. They also created a mechanism that safely resets the state of the dedicated SoC for use with other apps, so the state cannot be intercepted using any implicit or side channel. The reset is done using a detailed formal specification of hardware made on a Verilog-like language.

#SOSP19

During the third session speakers told about various debugging techniques.

The first guy told about a tool that can find a statement or instruction that causes a failure in parallel systems.

The next reporter gave an overview of their system for semantic fuzzing. During the presentation he demonstrated how this tool finds a bug in the mainline version of the F2FS filesystem. The reporter claims also that this system provides an OS-library based environment for execution of tests that is fully cleared between execution of every case.

The last report was dedicated to automatical detection of thread-safety violations without false positives. As I understood, this approach extends random delay instrumentation techniques with analyzing of timings between invocations of concurrently executed functions (methods).

#SOSP19

The conference hall.

#SOSP19

I have a little time to share my impressions of the fifth session of reports, which took place in the morning. All these reports were devoted to verification.

The first report described the Serval automated verification framework built on top of an SMT solver. The properties of the verified system can be described in a lisp-like language, after which they are given to the framework together with the verified program compiled into RISC-V binary code. The framework generates an input for the SMT solver.

The second report was about Perrenial - a framework for verification of concurrent and crash-safe systems. The researchers developed a concurrent mail server in golang and verified it using their framework.

The third speaker told about problems experienced during development of a verified filesystem (AtomFS) and a solution found in application of the concurrent relational logic with helpers.

The next speaker presented Vigor - a push-button easy to use tool for formal verification of network functions (NF). He said that the system requires writing very short specifications and it can be done even by developers without any knowledge in the verification topic. As I understood the system can extract protocol and header specifications automatically, because most of them are delivered as tables. The speaker said that tables are a kind of lingua franca of protocol specifications and this fact is used in Vigor.

#SOSP19

I saw the session seven yesterday, but all the reports were far enough from my sphere of interest.

The most interesting report was about a storage backend for Ceph. The researchers decided to remove a filesystem layer and do all the stuff closer to the hardware. The result outperformed the existing backends.

During session 8 I saw a presentation of guys from Google about their high performance networking stack moved to user space. Looks like this topic was already reported on conferences many times.

#SOSP19

Session eight was dedicated to NVM filesystems and database storage backends.

The first speaker from Australia told about KVell - a new key-value storage optimized for modern storage devices (nvme, intel optane, etc.). He said that buffering and delayed disk synchronisation can affect performance of databases negatively. Thus, the design for new fast storage devices need to avoid old solutions made for slow hard disks. As the result, KVell outperforms all modern key-value storages made for non-volatile memory systems.

The report was the only one that interested me a lot.

#SOSP19

There was also a session of reports made by students. Two of these presentations were interesting enough and won a prize. The gold prize has been given to the guy that described his work on power consumption profiling software for Linux. The silver prize went to the guy that developed an extension for Visual Studio Code for highlighting scopes of locks inside programs written in Rust.

#SOSP19

Spleeter is a python library and a command line tool for separating vocals, drums, piano, bass and other instruments in a given music track.

https://github.com/deezer/spleeter

The following guide shows how to create a simple Sqlite clone from scratch in order to understand how databases work.

https://cstack.github.io/db_tutorial/

During my studentship the demoscene consumed a lot of my spare time. I was just a spectator, not a demoscener, but knew very much in this area.

Now, I discover that many people don't know what the demoscene is. I looked for some good introductory article with a review of this layer of cyberculture, but didn't find anything that could fit my requirements.

Eventually I've found much, much more. The following tutorial not only tells what the demoscene is, it guides the beginner through creation of real artifacts like tracker music, demos, intros and publishing them on well known content hubs for demosceners.

https://github.com/psenough/teach_yourself_demoscene_in_14_days

I already mentioned the software made by Salvatore Sanfilippo including his tiny text editor named kilo. There is a detailed tutorial that shows how such editor can be written in 184 small steps. The author really starts from 3 lines of code and gradually extends the program.

https://viewsourcecode.org/snaptoken/kilo/

Small3dlib is a public domain 3D software rasterizer for constrained devices which uses only integer arithmetics.

https://gitlab.com/drummyfish/small3dlib

There is also a raycasting engine made by the same author.

https://gitlab.com/drummyfish/raycastlib

Surely many of us know Autodesk Inc. and its famous AutoCad, but few people know who John Walker is. He is the founder of Autodesk Inc. and a developer of the company's core products. In the next article, he tells how he wrote a neural network that recognized characters in 250 lines of BASIC for Commodore 64. He sent the program to all popular magazines about personal computing, but the program was not accepted for publication, as too esoteric. In 1987 neural networks were not so popular outside the academic community and few people understood why they were needed at all.

http://www.fourmilab.ch/documents/commodore/BrainSim/

A docker "analogue" written in bash.

https://github.com/p8952/bocker

AQaml is a self-hosted compiler for a rich subset of OCaml with pattern matching, variants, mutual recursion, references, GC and etc.

https://github.com/ushitora-anqou/aqaml

MAL is a variant of LISP that has 82 different implementations in various programming languages.

https://github.com/kanaka/mal/

Si78c is a pixel-accurate clone of the original Space Invaders game, it uses the original game resources and produces identical memory states during execution.

http://blog.loadzero.com/blog/si78c/

Unfortunately, Rui Ueyama stopped developing his optimizing C compiler (9cc), preferring the simpler chibicc, which is used as an example in his book (in Japanese). But it seems I found a replacement for 9cc, it is a small optimizing C compiler made by Lars Kirkholt Melhus. Lacc is easy to understand, self-hosting and actively developed.

lacc: https://github.com/larmel/lacc

Book written by Rui Ueyama: https://www.sigbus.info/compilerbook

In the following series on Medium Tomáš Bouda tells about 100 interesting algorithms for 100 days.

https://medium.com/100-days-of-algorithms