57
$\begingroup$

Since I left school (early 2010s) a couple of recently developed techniques were widely adopted by the industry. For example,

are some recent advances in computer science from the last decade that have 1) sound theoretical basis, are 2) implementable, and 3) have achieved some level of adoption in the industry (this last criterion is nice to have but not necessary).

I am interested in other examples that fulfill at least 2 out of the 3 (subjective :-) criteria that I enumerated. (For example, a new technique that has both (1) and (2) but has not yet been adopted is something I'd like to know about.)

$\endgroup$
13

10 Answers 10

34
$\begingroup$

Deriving fast JIT compilers from interpreters. It has long been known, that, in principle, compilers can be derived from interpreters in a mechanical way. This is a special case of partial evaluation, sometimes called Futamura projection [1]. The textbook [2] explains the state-of-the-art at the end of the 1990s. The core problem is that it has been difficult to get compilers derived by partial evaluation to match the performance of handwritten compilers ("O, Partial Evaluator, Where Art Thou?" L. Augustsson, 2010). In a parallel development, (tracing) JIT compilers emerged, their convoluted development might have started with [3]. The core problem with (tracing) JIT compilers is that they are complex, and expensive to develop.

Over the last few years, the situation changed.

  • Meta-tracing was developed [4] which turns an annotated interpreter into a tracing JIT compiler. This is the basis of PyPy [5] which is widely used [9].

  • In a parallel development, Oracle's new approach to Java compilation, Graal/Truffle [6, 7, 8], is based on partial evaluation, and indeed uses Futamura projections to convert an interpreter into a compiler (Graal is a conventional JIT and Truffle does the Futamura projection). It has been claimed that this is the first time that partial evaluation Futamura projection has led to a performant compiler.

There is clearly some family resemblance between meta-tracing and partial evaluation, but the exact relationship, the shared abstraction, is not fully understood.


[1] Y. Futamura, Partial Evaluation of Computation Process - An Approach to a Compiler-Compiler.

[2] J. Jones, C. K. Gormand, P. Sestoft, Partial Evaluation and Automatic Program Generation.

[3] J. G. Mitchell, The design and construction of flexible and efficient interactive programming systems.

[4] C. F. Bolz, A. Cuni, M. Fijalkowski, A. Rigo, Tracing the Meta-Level: PyPy's Tracing JIT Compiler.

[5] https://www.pypy.org/

[6] T. Würthinger, C. Wimmer, C. Humer, A. Wöß, L. Stadler, C. Seaton, G. Duboscq, D. Simon, M. Grimmer, Practical partial evaluation for high-performance dynamic language runtimes. https://chrisseaton.com/truffleruby/pldi17-truffle/pldi17-truffle.pdf

[7] https://github.com/oracle/graal/tree/master

[8] https://github.com/oracle/graal/tree/master/truffle

[9] https://news.ycombinator.com/item?id=36940871

$\endgroup$
2
  • 1
    $\begingroup$ The first usable version of PyPy was released in 2007; paper [4] (link here) was published in 2009. For clarity, it would be better to talk about RPython, the toolkit which builds PyPy; this toolkit was isolated in the early 2010s and is now available as a standalone package for non-PyPy usage. $\endgroup$
    – Corbin
    Sep 24 at 15:15
  • $\begingroup$ I recomend this book itu.dk/people/sestoft/pebook $\endgroup$
    – amirouche
    Oct 2 at 7:34
20
$\begingroup$

Low precision floating point data types. Historically, most programming used the IEEE 754 Standard for Floating-Point Arithmetic. Simplifying a great deal, IEEE 754 floats (64 bits version) give you

  • Lot of precision (53 bits mantissa).
  • Small exponent: 11 bits.

Historically, this was a good choice for many applications at the time. But it turns out that this was not good for deep learning. Simplifying a great deal:

  • Needs lots of memory for each floating point number.

  • Small exponent is problematic, because during training we often encounter extremely large or extremely small values.

  • High precision leads to overfitting, since high precision is a form of model capacity Having low precision arithmetic can be seen as a form of regularisation.

  • Maybe most important is the hardware perspecive:

    • Multiplication of exponents uses $O(n)$ transistors in the size of the exponent (multiplication of exponents is done by adding),
    • Multiplication of mantissa uses $O(n^2)$ transistors in the size of the mantissa.

By using less precision (mantissa) but bigger exponents we need fewer transistors per (floating point) arithmetic unit in processors, so we can pack more arithmetic units into each processor, which increases FP performance. This lead to experimentation and Google's first TPU uses the bfloat16 floating-point format

  • Sign bit: 1 bit
  • Exponent width: 8 bits
  • Mantissa: 7 bits
  • Different handling of underflows, overflows, and NaNs.

This lead to a flurry of activity, and modern CPUs and GPUs all provide for such low precision floating point numbers.

Given the preponderance of arithmetic units for low precision floating point arithmetic in modern processors, an interesting question is: how efficiently to bootstrap high-precision floating point operations from low precision floats?

(Note: I'm not sure about the history of low precision floats, that's why I'm not adding references. Feel free to edit.)

$\endgroup$
4
  • $\begingroup$ I don't see how that's a CS advance. For as long as FP have existed you could have made them with larger exponents and smaller mantissas. $\endgroup$ Sep 24 at 12:26
  • 2
    $\begingroup$ @toasted_flakes You can simulate the new short floats, but that would be much less efficient than having them as hardware primitives, presumably orders of magnitude less (just think about memory usage of your scheme, or transistors that are needed for IEEE 754 float multiplication vis-a-vis bfloat16). So I don't think you can simulate using comparable memory and transistor budget. Also, we have empirical evidence about the effect of different float formats on deep learning. None of this existed until recently. $\endgroup$ Sep 24 at 13:30
  • 1
    $\begingroup$ @toasted_flakes: I agree, it's not a new advance in computer science, it's just a case of different engineering tradeoffs for the same basic format becoming useful (and commercially relevant) for a new problem domain. The "science" part of this is the observation that deep-learning still works fine with few mantissa bits, enabling us to make that different engineering choice for an already-known approach to representing real numbers with fixed bit width. $\endgroup$ Sep 25 at 2:02
  • 1
    $\begingroup$ @toasted_flakes: A new approach to representing real numbers is the Posit, which avoids spending coding space on NaNs and Inf, and has gradual overflow for more dynamic range in limited bits, vs. IEEE FP having gradual underflow (subnormals) but hard overflow to +Inf. spectrum.ieee.org/floating-point-numbers-posits-processor / johndcook.com/blog/2018/04/11/anatomy-of-a-posit-number Posit support is even more limited in hardware that bfloat or IEEE FP16, but apparently Posit FPUs aren't too expensive to build. $\endgroup$ Sep 25 at 2:04
19
$\begingroup$

Liquid types. Introduced in [1], and refined in multiple follow-up papers. Liquid types can be seen as a form of dependent types that break with traditional type theory which is keen to have 'nice' typing rules that can be seen logical rules (this is the Curry-Howard perspective). Instead, liquid types are developed with a view towards maximising automation: all constraints during type-inference are simply handed to an SMT-solver, and automatically solved.

Liquid types are now used in industry for processor specification and verification through the Sail language [2], which is widely used, most prominently, for specifying the RISC-V instruction set architecture [3]. There are concerted efforts at augmenting general purpose languages with liquid types, in particular

  • Haskell [4]

  • Rust [5]

and probably more that I am not aware of.

(I used to be sceptical of using types much stronger than Damas-Hindley-Milner style Let-Polymorphism in general-purpose programming languages due to the loss of convenient type inference. Liquid types changed my mind.)


  1. P. M. Rondon, M. Kawaguchi, R. Jhala, Liquid Types. https://goto.ucsd.edu/~rjhala/papers/liquid_types.html

  2. A. Armstrong, T. Bauereiss, B. Campbell, A. Reid, K. E. Gray, M. Norton, P. Mundkur, M. Wassell, J. French, C. Pulte, S. Flur, I. Stark, N. Krishnaswami, P. Sewell, ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. https://github.com/rems-project/sail

  3. https://github.com/riscv/sail-riscv

  4. https://ucsd-progsys.github.io/liquidhaskell/

  5. N. Lehmann, A. Geller, N. Vazou, R. Jhala, Flux: Liquid Types for Rust. https://github.com/flux-rs/flux

$\endgroup$
16
$\begingroup$

Newer data structures. The mighty Bloom filter, which has been around since 1970, provides a way to store an approximation of a set of $n$ elements with false positive rate $\varepsilon$ using approximately $1.44 n \log_2 \varepsilon$ bits. In 2014 the cuckoo filter, based on cuckoo hashing, provided an alternative using approximately $1.08 n \log_2 \varepsilon + 3n$ bits while supporting deletions, while the 2019 XOR filter supports the set in $1.23 n \log_2 \varepsilon$ bits. While a full analysis of cuckoo filters is still open as of 2023, the theoretical basis for XOR filters is decently well understood and the connection to hypergraph peeling and orientability led to further improvements (most famously the Ribbon filter, which has been used at scale at Meta).

In 2017 the zip tree was invented, providing a way to build a randomized balanced binary search tree using $O(\log \log n)$ random bits per element. The height of zip trees slightly exceeds that of treaps, but in 2023 the zip-zip tree was introduced, which matches the theoretical guarantees of treaps using only $O(\log \log n)$ bits of randomness per element. To the best of my knowledge this data structure isn’t used in practice, but it’s definitely worth a look.

Just missing your cutoff, in 2009 the SA-IS algorithm for building suffix arrays was introduced. It runs in time $O(n)$ and is quite fast in practice. One of the most widely used suffix array construction algorithm libraries (LibDivSufSort) is based on the techniques developed in this algorithm.

$\endgroup$
3
  • 2
    $\begingroup$ Hollow heaps (2015) are another example of a direct improvement over an existing data structure. $\endgroup$ Sep 24 at 19:34
  • $\begingroup$ I’ve heard of hollow heaps but wasn’t aware that they were an improvement over other data structures. Can you elaborate? (I teach a course on “advanced” data structures and am always looking to modernize the syllabus!) $\endgroup$ Sep 25 at 1:27
  • $\begingroup$ Hollow heaps provide the same asymptotics as Fibonacci heaps, but improve the constant factors, which afaik are so high for the latter that it is never used in practice. $\endgroup$ Sep 26 at 5:26
15
$\begingroup$

Translation validation of compilers. In compilation, especially optimising compilation, correctness is a big issue for obvious reasons. Ideally, we'd like the whole compiler being proven correct once and for all, but this is beyond the state-of-the-art in 2023 for industrial strength compilers like LLVM and GCC (still there is progress, see CompCert [1] CakeML [2]).

However, we should not let the perfect be the enemy of the good: enter translation validation [3]. The idea is simple: instead of giving a single proof that the compiler is correct for all input programs $P$, we prove, for an individual program $P$ that the translation of $P$ is correct. This is much less demanding. Note that proving that the compiler correctly translates a given program $P$, does not imply that it also translates other programs correctly! That may sound really weak, but, empirically, translation validation is useful [4, 5, 6]:

  • Translation validation (at least of individual optimisation passes) can be automated with SMT solvers like Z3, even for complex LLVM optimisation passes.

  • Doing translation validation for a modest size number of programs finds huge number of bugs in complex LLVM optimisation passes automatically

This raises more questions: for example, is the translation validator itself correct? See [7] for recent progress in this direction.


[1] X. Leroy, Formal verification of a realistic compiler. https://xavierleroy.org/publi/compcert-CACM.pdf

[2] https://cakeml.org/

[3] A. Pnueli, M. Siegel, E. Singerman, Translation Validation.

[4] N. P. Lopes, D. Menendez, S. Nagarakatte, J. Regehr, Provably Correct Peephole Optimizations with Alive.

[5] N. P. Lopes, J. Lee, C.-K. Hur, Z. Liu, J. Regehr, Alive2: Bounded Translation Validation for LLVM.

[6] https://github.com/AliveToolkit/alive2

[7] J. Lee, C.-K. Hur, N. P. Lopes, AliveInLean: A Verified LLVM Peephole Optimization Verifier.

$\endgroup$
15
$\begingroup$

async/await pattern

I'm not really sure how well this fits the criteria (especially the "since 2010" part is kinda fuzzy here), but I myself consider this to be the most significant practical advance in the last decade.

In and of itself it's not really that revolutionary - it's really just a bit of syntax sugar on top of concepts that already existed before (Promises, coroutines, asynchronous IO), but the impact it has is nothing short of staggering. While asynchronous IO was possible before async/await in various ways, it was always difficult and awkward to write such programs. async/await turned that around completely. Suddenly asynchronous IO became trivial to do and this has resulted in orders of magnitude performance increases.

About the timeline - although the roots of this idea are much older, the first async/await implementation came in C# in 2012. From this the feature spread rapidly to other languages like Haskell, Python, TypeScript, JavaScript, Rust, Swift and even C++.

$\endgroup$
7
  • 2
    $\begingroup$ At least Twisted (Python networking library) had inlineCallbacks, an async/await implementation, in 2008. They may have had it even earlier, but I can't track down a precise date. $\endgroup$
    – Corbin
    Sep 24 at 15:12
  • $\begingroup$ The async/await pattern seems to have first appeared in Haskell around 1999 (e.g. A poor man's concurrency monad). async/await is a limited form of delimited continuation (like many other 'control-flow pairs', e.g. try/throw, call/early-return, for/yield, etc.); those date back to the 1980s and are commonly used for coroutines (though I'm not sure when the exact pattern of async/await appeared) $\endgroup$
    – Warbo
    Sep 28 at 11:06
  • $\begingroup$ @Warbo I'm... not sure where it fits in the pure theory world. But I also cannot see how one could use, say, try/catch to implement something similar to await/async. I know that there are implementations that (ab)use for/yield, although I think that not every language's for/yield is suited for this purpose either. Anyway they are not as elegant as the dedicated await/async. $\endgroup$
    – Vilx-
    Sep 28 at 11:51
  • $\begingroup$ @Vilx- Sorry, I may have been confusing: "delimited continuations" are a powerful language feature dating back to ~1988; shift/reset is the most common form. If you have shift/reset, you can implement async/await as a library; you can also implement try/catch, for/yield, etc. too. Delimited continuations can be thought of as "resumable exceptions" (related to Algebraic Effects), "exceptions with state", "non-linear yield", or "the mother of all monads" $\endgroup$
    – Warbo
    Sep 28 at 12:20
  • 2
    $\begingroup$ @Warbo - Well, as I said, the base ideas are not new, but it's this particular... manifestation (implementation?) of them that has turned out to be wildly successful. $\endgroup$
    – Vilx-
    Sep 28 at 12:49
7
$\begingroup$

There is a lot going on in cryptography.

This post is community wiki; hopefully others can expand.

$\endgroup$
5
$\begingroup$

CRDT (Conflict-free replicated data type), data structure used for decentralized real-time editors, has been formally defined in 2011, according to wikipedia. Industry adoption is also mentioned in the same wikipedia page

$\endgroup$
1
  • $\begingroup$ Yes. Research on the verification of CRDTs and algos based on CRDT is also very active. $\endgroup$ Sep 25 at 18:07
5
$\begingroup$

Differential privacy, a technique for analyzing data and releasing statistics privately, was in its infancy in 2010 and has since had a lot of development and advances, and adoption by major web browsers for telemetry, the U.S. 2020 Census, and probably numerous other places.

$\endgroup$
4
$\begingroup$

There have been numerous advances in machine learning since 2010. Most of the highly impactful advances are not fully theoretically sound, but most of them involve some theoretical backings, to greater and lesser extents.

  • progress in convex and non-convex optimization
  • game-playing, regret minimization
  • neural network architectures, evaluation, and training methods
  • reinforcement learning, recommendation algorithms
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.