Zero Dereference – Telegram
Zero Dereference
127 subscribers
3 photos
3 files
372 links
Interesting links related to systems programming, hacking, and science.

Contact: @richiefreedom
Download Telegram
On his YouTube channel Luke Smith talks about various lightweight UNIX tools with suckless philosophy. He also has a number of exciting videos on history, politics and Latin.

https://youtube.com/c/lukesmithxyz
The best way to learn the ARMv8 assembly language is reading of ARMARM (ARM Architecture Reference Manual), but if you have no time and need to master only application-level assembly programming — some short tutorial would be enough. One of them can be found below. This tutorial gives an overview of ARMv8, its instruction set and common code patterns. It also shows how various cryptograpic algorithms can be implemented using the assembly language.

https://modexp.wordpress.com/2018/10/30/arm64-assembly/
For a long time I have been collecting examples of extremely tiny software for embedded applications. The following library written by Adam Dunkels was one of the first citizens of the collection. Protothreads provides a kind of coroutines with very little overhead (2 bytes per "thread"), moreover it doesn't use any architecture-dependent context switching code - all the magic is done using a layer of well-organized macros, generating state machines inside functions.

http://dunkels.com/adam/pt/
Have you heard about any fork or alternative distribution of TempleOS? It exists! Shrine is a distribution of Temple OS with traditional UNIX-like shell, networking, package management and lower memory consumption.

https://github.com/minexew/Shrine
TempleOS is an alien operating system. It uses own programming language, own concept of document-oriented user interface, it can be developed only on TempleOS itself.

If somebody wants to add a new application to this OS, the system forces him/her to use HolyC and uncommon system libraries. But most of the systems software today is written in C. Writing this application in C would be a good idea, right?

In his blog post Jack Whitham shows the way to port C programs to TempleOS by implementation of a loader in HolyC, which can load object files built for another operating system. He also made a port of uclibc to run unmodified software made in conformance with the C standard.

https://www.jwhitham.org//2015/07/porting-third-party-programs-to-templeos.html
The JVM compiler interface allows you to replace the default JIT compiler by your own, written in Java. Graal uses this interface to get its job done. You can find more details by clicking the link below.

https://chrisseaton.com/truffleruby/jokerconf17/
I have seen many object systems for C. Most of them used the macro language of the C preprocessor to generate boilerplate code emulating classes and objects with the flavour of C++.

The following solution is totally different. It resembles the object systems of Common Lisp and Objective C. It uses crazy macro-magic to parse new OO-related keywords. Parsing with macros, is it really possible? Yes, the authors use a kind of functional language implemented on top of the C preprocossor's language to safely transform its input and provide meaningful error messages. The system implements multi-dispatch and multi-forwarding of messages, generics, contracts and exceptions.

https://arxiv.org/pdf/1003.2547.pdf
Linus Åkesson noticed that Unix pipes connecting /dev/zero and /dev/null resemble electrical circuits. He wrote a program that implements an analogue of a transistor and made basic logic gates. Thus, it is possible to make a processor and do arbitrary computing.

https://www.linusakesson.net/programming/pipelogic/index.php
There is always a gap between the denoscription of an algorithm and its commercial implementation. For example, popular libraries for decoding images look very monstrous. This is due to the fact that their code is highly optimized, they support many versions of fomats that they work with, etc. One gets the impression that the data formats themselves are just as complex. But this is a false feeling. Compact and clear library implementations are possible. A good example is the implementation of the JPEG decoder in Python 3, which fits in 250 lines of clear code. Yes, this code does not work as fast as libjpeg or libjpeg turbo, but it is already good enough. A small investment of time in optimization can make it suitable for use even in commercial projects. By the way, a variant of this program, rewritten in C, is used in ToaruOS, one of the most impressive amateur operating systems.

https://github.com/aguaviva/micro-jpeg-visualizer
It turns out that there is a concise free book on algorithms with an emphasis on competitive programming.

https://cses.fi/book/book.pdf
Do you remember the article of Linus Åkesson about logic gates built for Unix pipes-centric model of electrical circuits? He made another strange computing machine built around Unix symlinks.

https://www.linusakesson.net/programming/symlinks/index.php
In a day, the biennial ACM Symposium on Operating Systems Principles will begin in Canada. Yesterday I flew to Toronto and plan to go to Huntsville by the beginning of the event. So, I will have the opportunity to write short notes on the topics reported or discussed on the conference.

https://sosp19.rcs.uwaterloo.ca/

#SOSP19
Zero Dereference pinned «In a day, the biennial ACM Symposium on Operating Systems Principles will begin in Canada. Yesterday I flew to Toronto and plan to go to Huntsville by the beginning of the event. So, I will have the opportunity to write short notes on the topics reported or…»
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