HN user

matt_d

20,521 karma
Posts3,017
Comments134
View on HN
orenlab.cis.bgu.ac.il 1h ago

Drawn Apart: Remote GPU Fingerprinting

matt_d
2pts0
icfpcontest2026.com 2h ago

ICFP Programming Contest 2026

matt_d
3pts0
redplait.blogspot.com 2h ago

Optimization of SASS Stall Counts

matt_d
1pts0
muratbuffalo.blogspot.com 15h ago

Characterizing Metastable Faults and Failures

matt_d
1pts0
arxiv.org 2d ago

Every Microsecond Matters:Achieving Near SpeedOfLight Latency in GPU Collectives

matt_d
2pts0
rocm.blogs.amd.com 2d ago

SPIR-V on ROCm: A Portable IR for AMD GPUs

matt_d
5pts2
docs.nvidia.com 2d ago

GEMM Performance Measurement Methodology Guidelines

matt_d
1pts0
dl.acm.org 2d ago

Faster Algorithms for Structured Matrix Multiplication via Flip Graph Search

matt_d
1pts0
dl.acm.org 3d ago

AI for Systems is "AGI-Complete"

matt_d
3pts0
magazine.sebastianraschka.com 4d ago

Controlling Reasoning Effort in LLMs

matt_d
1pts0
www.philipzucker.com 5d ago

Making TLA+ and x86 Kiss via Z3Py

matt_d
4pts0
maskray.me 5d ago

Irreducible Loops

matt_d
3pts0
arxiv.org 6d ago

Fleet: Hierarchical Task-Based Abstraction for Megakernels on Multi-Die GPUs

matt_d
10pts1
dl.acm.org 6d ago

Accelerating Block Low-Rank Foundation Model Inference on MemoryConstrained GPUs

matt_d
10pts0
dl.acm.org 7d ago

Locality-Aware Automatic Differentiation on the GPU for Mesh-Based Computations

matt_d
2pts0
pytorch.org 7d ago

Triton Plugin Extensions: Enabling TLX and Custom Compiler Passes Out of the Box

matt_d
3pts0
hanchenli.github.io 7d ago

What If the Harness Comes Before Pretraining? A Data Flywheel Perspective

matt_d
2pts0
www.usenix.org 7d ago

Mimesys: Turn Resource Usage Traces into Executable Workloads

matt_d
3pts1
www.humprog.org 8d ago

System call instrumentation on Linux/x86-64 using memory-indirect calls

matt_d
2pts1
arxiv.org 8d ago

Bidirectional Elaborators à la Carte

matt_d
3pts0
arxiv.org 8d ago

CTA-Pipelining: A Latency-Oriented Spatial Scaling Method for Multi-GPU Systems

matt_d
2pts0
developer.nvidia.com 10d ago

AI Model Co-Design: Hardware-Friendly LLM Design

matt_d
2pts0
pytorch.org 10d ago

Towards Free Normalization: Fusing Normalization into GEMM and Attention Kernels

matt_d
2pts0
gupea.ub.gu.se 10d ago

Negotiating AI in Open Source Software Communities: A Case Study of LLVM Project

matt_d
2pts0
developer.nvidia.com 10d ago

Reducing HBM Bottlenecks in JAX-Based LLM Training with Host Offloading

matt_d
2pts0
nowarp.io 10d ago

Compiler Testing – Part 2: Metamorphic Testing with Verified Identities

matt_d
2pts0
labs.quansight.org 11d ago

What Every Python Developer Should Know About the CPython ABI

matt_d
74pts5
samuelcoward.co.uk 11d ago

A CIRCT (Circuit IR Compilers and Tools) Project Tutorial

matt_d
1pts0
www.philipzucker.com 11d ago

Lifting Terms: Making Well Scoped Syntax Dumber

matt_d
1pts0
www.tweag.io 11d ago

Sheaves in Haskell

matt_d
2pts0

Looks interesting!

Out of curiosity, how does it compare with vLLM Semantic Router?

For reference:

https://vllm-semantic-router.com/

https://github.com/vllm-project/semantic-router

vLLM Semantic Router: Signal Driven Decision Routing for Mixture-of-Modality Models, https://arxiv.org/abs/2603.04444

https://github.com/vllm-project/semantic-router

For instance, does it offer similar algorithms:

- vllm-sr/auto: efficient, fast, balanced routing, similar in spirit to Fugu // Sakana Fugu — Multi-Agent System as a Model: https://sakana.ai/fugu/ - vllm-sr/fusion: panel-style multi-model reasoning and synthesis. - vllm-sr/flow: router-native workflow orchestration - vllm-sr/remom: multi-round reasoning over one or multiple models.

FWIW, it does look good on https://routeworks.github.io/leaderboard

Ref.

RouterArena: An Open Platform for Comprehensive Comparison of LLM Routers, https://arxiv.org/abs/2510.00202, https://github.com/RouteWorks/RouterArena

Pretty nifty work; more details (full type system specification, including type inference rules, collective signatures, and forward-backward pairs):

https://github.com/meta-pytorch/spmd_types/blob/main/DESIGN....

I'd also recommend the series of posts by Edward:

- https://blog.ezyang.com/2026/01/global-vs-local-spmd/

- https://blog.ezyang.com/2026/01/jax-sharding-type-system/

- https://blog.ezyang.com/2026/02/dtensor-erasure/

- https://blog.ezyang.com/2026/02/replicate-forwards-partial-b...

Also interesting:

AutoParallel: a PyTorch library that automatically shards and parallelizes models for distributed training. Given a model and a device mesh, it uses linear programming to find an optimal sharding strategy (FSDP, tensor parallelism, or a mix) and applies it — no manual parallelism code required.

https://github.com/meta-pytorch/autoparallel

AutoParallel is a PyTorch library that automatically shards and parallelizes models for distributed training. Given a model and a device mesh, it uses linear programming to find an optimal sharding strategy (FSDP, tensor parallelism, or a mix) and applies it — no manual parallelism code required.

Slides (PDF): https://compiler-research.org/assets/presentations/Aaron_Vip...

Abstract: https://compiler-research.org/presentations/#USINGSTDCPP2026

Despite its high-performance capabilities, C++ is not the first programming language that comes to mind for rapidly developing robust applications, mainly due to the long edit-compile-run cycles. Ongoing research in the compiler-research.org group aims to provide practical, interactive capabilities for C++, enabling dynamic interoperability, rapid prototyping, and exploratory programming, essential for data science and other applications. This talk explores how interactive C++ can be leveraged for various scientific usecases and teaching. Attendees will also learn how to leverage Clang as a library to build a simple C++ REPL for incremental compilation and introspection, integrating this layer with the Python runtime.

The second part of this talk covers CppInterOp, a production-grade C++ interoperability library based on LLVM and Clang that provides compiler-as-a-service capabilities for seamless cross-language integration. CppInterOp formalizes a stable, backward-compatible API that enables dynamic languages to harness the full power of modern C++ without sacrificing expressiveness or performance. We explore applications of the CppInterOp library in the context of Python/C++ bindings, interactive C++ notebooks with xeus-cpp, and WebAssembly.

Repo:

K-Search: LLM-Driven GPU Kernel Optimization with Co-Evolving Intrinsic World Model, https://github.com/caoshiyi/K-Search

K-Search is an automated kernel engineering system that uses large language models (GPT-5, Gemini etc.) to iteratively generate and optimize GPU kernels. Unlike one-shot code generation, K-Search maintains a co-evolving world model — a structured search tree that encodes hypotheses about kernel bottlenecks, design alternatives, and optimization strategies — guiding multi-round, evidence-driven search over the kernel design space efficiently.

Paper: https://doi.org/10.1145/3695053.3731011

PDF: https://dl.acm.org/doi/pdf/10.1145/3695053.3731011

Abstract: This paper introduces Heliostat, which enhances page translation bandwidth on GPUs by harnessing underutilized ray tracing accelerators (RTAs). While most existing studies focused on better utilizing the provided translation bandwidth, this paper introduces a new opportunity to fundamentally increase the translation bandwidth. Instead of overprovisioning the GPU memory management unit (GMMU), Heliostat repurposes the existing RTAs by leveraging the operational similarities between ray tracing and page table walks. Unlike earlier studies that utilized RTAs for certain workloads, Heliostat democratizes RTA for supporting any workloads by improving virtual memory performance. Heliostat+ optimizes Heliostat by handling predicted future address translations proactively. Heliostat outperforms baseline and two state-of-the-arts by 1.93 ×, 1.92 ×, and 1.66 ×. Heliostat+ further speeds up Heliostat by 1.23 ×. Compared to an overprovisioned comparable solution, Heliostat occupies only 1.53% of the area and consumes 5.8% of the power.

Paper (PDF): https://2plus2a.com/files/publications/2025-ISCA-precise-exc..., https://2plus2a.com/publications/errata#exc-isca25

DOI: https://doi.org/10.1145/3695053.3731102

Abstract:

To manage exceptions, software relies on a key architectural guarantee, precision: that exceptions appear to execute between instructions. However, this definition, dating back over 60 years, fundamentally assumes a sequential programmers model. Modern architectures such as Arm-A with programmer-observable relaxed behaviour make such a naive definition inadequate, and it is unclear exactly what guarantees programmers have on exception entry and exit.

In this paper, we clarify the concepts needed to discuss exceptions in the relaxed-memory setting – a key aspect of precisely specifying the architectural interface between hardware and software. We explore the basic relaxed behaviour across exception boundaries, and the semantics of external aborts, using Arm-A as a representative modern architecture. We identify an important problem, present yet unexplored for decades: pinning down what it means for exceptions to be precise in a relaxed setting. We describe key phenomena that any definition should account for. We develop an axiomatic model for Arm-A precise exceptions, tooling for axiomatic model execution, and a library of tests. Finally we explore the relaxed semantics of software-generated interrupts, as used in sophisticated programming patterns, and sketch how they too could be modelled.

Some highlights (by Stuart Sul):

Tensor core and memory pipelining: it turns out some tensor core instructions are implicitly pipelined, without proper documentation. Identifying these implicit semantics and the resulting pipelining tactics can boost your throughput by up to 10%.

Hinting the PTX assembler properly: even logically identical PTX code can compile into meaningfully different SASS instructions, depending on how you write it. Signaling the assembler with the right instruction patterns is significant for minimizing latency.

Occupancy: with all the modern GPU features, it gets tricky, and it is (again) poorly documented. Distributed shared memory doesn’t behave identically across all SMs, and 5th-generation tensor core instructions silently cap occupancy.

Main takeaway:

Our experiments show that Intel’s port assignment policies can diverge significantly from the well-documented "least-loaded eligible port" model, illustrated in Figure 1. Using carefully crafted two-instruction microbenchmarks preceded by an LFENCE, we consistently observed dynamic scheduling policies. Instead of a fixed distribution across eligible ports, the port assignment changes as the unroll factor increases, producing distinct regions separated by cutoffs. As illustrated in Figure 2 for the “LFENCE; CBW; CBW” snippet, the port scheduler employs three different strategies depending on the number of loop iterations. At lower unroll factors, one sparsest port is strongly preferred. After a first cutoff, the allocation becomes approximately uniform across all eligible ports, albeit noisy. At a second cutoff, the scheduler shifts again, favoring a different subset of ports. The second cutoff’s unroll factor is twice the first’s unroll factor. These dynamics are not isolated: we observed similar cutoff-based transitions across multiple instructions and instruction pairs, and in some cases, the behavior also depends on the order of instructions in the block or on immediate values used in operands. We believe that this might serve as a new microarchitectural attack surface which can be harnessed towards implementing, e.g., covert channels, fingerprinting, etc. Importantly, the observed cutoffs are consistent and reproducible across multiple runs, but differ between CPU generations. These findings show that static eligibility sets cannot fully describe port assignment. Instead, the allocator follows multiple hidden policies, switching between them in ways not accounted for by existing models.

Paper: https://dl.acm.org/doi/10.1145/3759164.3759346

Haskell & Agda Code: https://doi.org/10.5281/zenodo.16751639

Abstract: https://bahr.io/pubs/entries/calctyper.html

We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. We focus on languages whose semantics can be expressed as a fold, and show how the calculations can be simplified using fold fusion. This approach enables the compositional derivation of correct-by-construction type checkers based on solving and composing fusion preconditions. We introduce our approach using a simple expression language, to which we then add support for exception handling and checked exceptions.

Announcement:

https://mathstodon.xyz/@andrejbauer/115191725004191889

This week I gave a lecture series at the School on Logical Frameworks and Proof Systems Interoperability. I spoke about programming language techniques for proof assistants. The lecture slides and the reference implementations of a minimalist type theory are available at:

https://github.com/andrejbauer/faux-type-theory

The repository has three minimalist OCaml implementations of a simple proof checker:

1. A basic one showing how to implement bidirectional type checking and type-directed equality checking, using monadic style programming.

2. An extension with rudimentary holes (meta-variables) and unification.

3. A version that implements "variables as computational effects", using native OCaml 5 effects and handlers.

As far as compiling continuations goes, sequent calculus (specifically as a compiler IR) is an interesting research direction. See Grokking the Sequent Calculus (Functional Pearl) from ICFP 2024: https://dl.acm.org/doi/abs/10.1145/3674639

"This becomes clearer with an example: When we want to evaluate the expression (2 + 3) ∗ 5, we first have to focus on the subexpression 2 + 3 and evaluate it to its result 5. The remainder of the program, which will run after we have finished the evaluation, can be represented with the evaluation context □ ∗ 5. We cannot bind an evaluation context like □ ∗ 5 to a variable in the lambda calculus, but in the λμ~μ-calculus we can bind such evaluation contexts to covariables. Furthermore, the μ-operator gives direct access to the evaluation context in which the expression is currently evaluated.

Having such direct access to the evaluation context is not always necessary for a programmer who wants to write an application, but it is often important for compiler implementors who write optimizations to make programs run faster. One solution that compiler writers use to represent evaluation contexts in the lambda calculus is called continuation-passing style. In continuation-passing style, an evaluation context like □ ∗ 5 is represented as a function λ x . x ∗ 5. This solution works, but the resulting types which are used to type a program in this style are arguably hard to understand. Being able to easily inspect these types can be very valuable, especially for intermediate representations, where terms tend to look complex. The promise of the λμ~μ-calculus is to provide the expressive power of programs in continuation-passing style without having to deal with the type-acrobatics that are usually associated with it."

A brief summary of the SC-as-a-compiler-IR vs. CPS from one of the authors of the paper: https://types.pl/@davidb/115186178751455630

"In some sense the Sequent Calculus (SC) is quite similar to a CPS based IR. To sum up the benefits of SC over CPS in two concepts, I would say: Symmetry and non-opaque continuations.

Symmetry: A lot of pairs of dual concepts are modelled very naturally and symmetrically in SC: call-by-value and call-by-name, data types and codata types, exception based error handling and Result-type error handling, for example.

Non-Opaque continuations: Instead of continuations in CPS which are just a special kind of function whose internals cannot be inspected (easily), SC introduces consumers whose internal structure can be inspected easily, for example when writing optimization passes."

Abstract:

Programs written in C/C++ often include inline assembly: a snippet of architecture-specific assembly code used to access low-level functionalities that are impossible or expensive to simulate in the source language. Although inline assembly is widely used, its semantics has not yet been formally studied.

In this paper, we overcome this deficiency by investigating the effect of inline assembly to the consistency semantics of C/C++ programs. We propose the first memory model of the C++ Programming Language with support for inline assembly for Intel’s x86 including non-temporal stores and store fences. We argue that previous provably correct compiler optimizations and correct compiler mappings should remain correct under such an extended model and we prove that this requirement is met by our proposed model.

Paper: https://doi.org/10.1145/3689749

Slides: https://devilhena-paulo.github.io/files/inline-x86-asm-slide...

Afterword:

"This pearl grew out of the authors’ frustration with textbook presentations of binary search. Given that binary search is one of the standard algorithms every programmer and computer science student should know, the subject is inadequately covered at best. Many textbooks mention binary search only in passing or they treat only special cases, such as computing the square root or searching an ordered table. A negative mindset prevails: the search possibly fails; in the divide&conquer step one half of the search space is excluded from consideration because searching this half will definitely fail. The correctness argument requires that the data is ordered, suggesting that monotonicity in some sense drives the search. One notable exception is Anne Kaldewaij’s textbook (Reference Kaldewaij1990): when discussing “function inversion” (given n , find an argument i such that fi⪯n≺f(1+i) ) he emphasises repeatedly that the correctness of the search does not require that f is an ascending function.

The gist of this pearl is to approach search problems with a positive mind-set: the search always succeeds; in the divide&conquer step the search continues with the half that guarantees success. The correctness argument relies on a suitable functional invariant, not on monotonicity. The “Beat Your Neighbours!” problem, a concrete make-up for local maximum search, shows that the extra generality is actually needed."

Start here: "The Microarchitecture of Superscalar Processors," J.E. Smith and G.S. Sohi, Proc. IEEE, vol. 83 (1995) https://doi.org/10.1109/5.476078 https://courses.cs.washington.edu/courses/cse471/01au/ss_cgi...

It's very brief (so if you only have time to read one thing you won't waste a single minute: it's to the point) and (perhaps surprisingly, given its publication date) highly relevant: In fact, right after reading Section IV.C (AMD K5) you should be able to immediately jump to and understand the microarchitectural diagrams of, say, AMD Zen 2: http://web.archive.org/web/20231213180041/https://en.wikichi... http://web.archive.org/web/20231213180041/https://en.wikichi... ...and any other contemporary CPU.

Smith & Sohi paper is going to give you great intuition for what's essentially implemented by all modern CPUs: restricted dataflow (RDF) architecture.

A great follow-up is a short blog post "A whirlwind introduction to dataflow graphs" by Fabian “ryg” Giesen: https://fgiesen.wordpress.com/2018/03/05/a-whirlwind-introdu...

For context, all superscalar dynamically scheduled (out-of-order) CPUs implement RDF, introduced by Yale Patt's research group's work on High Performance Substrate (HPS). This work pretty much defined the modern concept of a restricted dataflow CPU: breaking complex instructions into smaller micro-operations and dynamically scheduling these to execute out-of-order (or, to be more specific, in a restricted dataflow order) on multiple execution units.

(If you're curious, the "restricted" part comes from the finite instruction window delimiting the operations to be scheduled, which stems from the finite size of all the physical resources in real hardware, like the ROB/reorder buffer. The "dataflow" comes from having to respect data dependencies, like `A = 1` and `B = 2` having to execute before `C = A + B`, or `MOV A, 1` and `MOV B, 2` having to execute before `ADD C, A, B`; but note that you can freely reorder the aforementioned moves among themselves as long as you execute them before the add: a schedule/execution order of `MOV B, 2; MOV A, 1; ADD C, A, B` is just as valid).

For the historical background, see "HPS papers: A retrospective", https://www.researchgate.net/publication/308371952_HPS_paper... (Minor per peeve warning:) It also sets the record straight w.r.t. to the RISC being orthogonal to the historical development of modern superscalar out-of-order CPUs: In particular, it's worth noting that the aforementioned micro-operations have absolutely _nothing_ to do with RISC! Another great resource on that is Fabian's video "CPU uArch: Microcode", https://www.youtube.com/watch?v=JpQ6QVgtyGE (also worth noting that micro-operations and microcode are _very_ different concepts; that's also very well covered by the video).

Another good, succinct description of the historical background is the 2024 IEEE CS Eckert-Mauchly Award (Wen-mei Hwu was a PhD student in the aforementioned Yale Patt's group): "Hwu was one of the original architects of the High-Performance Substrate (HPS) model that pioneered superscalar microarchitecture, introducing the concepts of dynamic scheduling, branch prediction, speculative execution, a post-decode cache, and in-order retirement." - https://www.acm.org/articles/bulletins/2024/june/eckert-mauc...

On a side note, load-store architecture introduced by CDC 6600 (designed by Seymour Cray in the 1960s) is sometimes mistaken for RISC (which came decade+ later, arguably introduced in IBM 801 designed by John Cocke in the late 1970s/early 1980), https://en.wikipedia.org/wiki/Load%E2%80%93store_architectur...

One could say load-store architecture does have an influence on compiler backends implementation, after a fashion (thinking of instruction scheduling, with a complex operation combining, say, LOAD with arithmetic operation OP, broken down in the scheduling models as separate LOAD and OP operations/effects).

For more, I'd recommend:

"Performance Analysis and Tuning on Modern CPU" by Denis Bakhvalov https://github.com/dendibakh/perf-book/releases

Agner Fog's Optimization Manuals https://www.agner.org/optimize/

Prof. Onur Mutlu's Lecture Videos and Materials https://people.inf.ethz.ch/omutlu/lecture-videos.html

These are absolutely fantastic--I've followed all of these a few years back and can vouch for the quality and being up-to-date or at least decades ahead of the general computer architecture textbooks: the lectures and readings cover contemporary work including ISCA and MICRO papers that have only recently found their way to the implementation in production CPUs (e.g., the hashed perceptron predictor that's one of the branch predictor units in AMD Zen 2, http://web.archive.org/web/20231213180041/https://en.wikichi...).

There are more, topic-specific texts that are very good, e.g., A Primer on Memory Consistency and Cache Coherence, Second Edition; Synthesis Lectures on Computer Architecture 15:1 (2020); Vijay Nagarajan, Daniel J. Sorin, Mark D. Hill, David A. Wood; open access (freely available) at https://doi.org/10.2200/S00962ED2V01Y201910CAC049 but when you are at this point you're likely going to be good at finding the relevant resources yourself, so I'm going to leave it to you to explore further :-)

Background:

https://discourse.llvm.org/t/announcing-the-lifetime-safety-...

Lifetime Analysis: Current Status

For those not already familiar, we’re working on a new lifetime analysis in Clang to catch issues like use-after-scope or returning pointers to stack memory. The analysis is alias-based and draws inspiration from Rust’s borrow checker (specifically, [Polonius](https://smallcultfollowing.com/babysteps/blog/2018/04/27/an-...)). More details in the RFC: https://discourse.llvm.org/t/rfc-intra-procedural-lifetime-a...

The initial implementation targets intra-procedural analysis for C++ raw pointers. This keeps the surface area small while we iterate. Over time, we aim to enable this analysis by default in Clang, with both “permissive” and “strict” modes to balance noise and coverage.

Key Components

- Conceptual Model: Introduces the fundamental concepts of Loan, Origin, and Path to model memory borrows and the lifetime of pointers.

- Fact Generation: A frontend pass traverses the Clang CFG to generate a representation of lifetime-relevant events, such as pointer assignments, taking an address, and variables going out of scope.

- Testing: llvm-lit tests validate the analysis by checking the generated facts.

Example:

[LifetimeSafety] Introduce intra-procedural analysis in Clang

Commit: https://github.com/llvm/llvm-project/commit/3076794e924f

PR: https://github.com/llvm/llvm-project/pull/142313

Test source code: https://github.com/llvm/llvm-project/blob/3076794e924f30ae21...

Rex Kernel Extensions: a safe and usable kernel extension framework that allows loading and executing Rust kernel extension programs in the place of eBPF

https://github.com/rex-rs/rex

Abstract:

"Safe kernel extensions have gained significant traction, evolving from simple packet filters to large, complex programs that customize storage, networking, and scheduling. Existing kernel extension mechanisms like eBPF rely on in-kernel verifiers to ensure safety of kernel extensions by static verification using symbolic execution. We identify significant usability issues—safe extensions being rejected by the verifier—due to the language-verifier gap, a mismatch between developers’ expectation of program safety provided by a contract with the programming language, and the verifier’s expectation.

We present Rex, a new kernel extension framework that closes the language-verifier gap and improves the usability of kernel extensions in terms of programming experience and maintainability. Rex builds upon language-based safety to provide safety properties desired by kernel extensions, along with a lightweight extralingual runtime for properties that are unsuitable for static analysis, including safe exception handling, stack safety, and termination. With Rex, kernel extensions are written in safe Rust and interact with the kernel via a safe interface provided by Rex’s kernel crate. No separate static verification is needed. Rex addresses usability issues of eBPF kernel extensions without compromising performance."

Abstract:

"Extensions allow applications to expand the capabilities of database management systems (DBMSs) with custom logic. However, the extensibility environment for some DBMSs is fraught with perils, causing developers to resort to unorthodox methods to achieve their goals. This paper studies and evaluates the design of DBMS extensibility. First, we provide a comprehensive taxonomy of the types of DBMS extensibility. We then examine the extensibility of six DBMSs: PostgreSQL, MySQL, MariaDB, SQLite, Redis, and DuckDB. We present an automated extension analysis toolkit that collects static and dynamic information on how an extension integrates into the DBMS. Our evaluation of over 400 PostgreSQL extensions shows that 16.8% of them are incompatible with at least one other extension and can cause system failures. These results also show the correlation between these failures and factors related to extension complexity and implementation."

Database Extensions Analyzer: https://github.com/cmu-db/ext-analyzer

Talk: https://www.youtube.com/watch?v=U7v0fubktoY

Preprint: https://williamjbowman.com/resources/wjb2024-ethical-compile...

DOI: https://doi.org/10.1145/3704253.3706135

William J. Bowman. The 2025 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM) – Invited Talk.

Abstract:

"The is-ought gap is a problem in moral philosophy observing that ethical judgments ("ought") cannot be grounded purely in truth judgments ("is"): that an ought cannot be derived from an is.

This gap renders the following argument invalid: "It is true that type safe languages prevent bugs and that bugs cause harm, therefore you ought to write in type safe languages".

To validate ethical claims, we must bridge the gap between is and ought with some ethical axiom, such as "I believe one ought not cause harm".

But what do ethics have to do with manipulating programs?

A lot!

Ethics are central to correctness!

For example, suppose an algorithm infers the type of is Bool, and is in fact a Bool; the program type checks.

Is the program correct-does it behave as it ought?

We cannot answer this without some ethical axioms: what does the programmer believe ought to be?

I believe one ought to design and implement languages ethically.

We must give the programmer the ability to express their ethics-their values and beliefs about a program-in addition to mere computational content, and build tools that respect the distinction between is and ought.

This paper is a guide to ethical language design and implementation possibilities."

3-min talk: https://www.youtube.com/watch?v=791PEI35tio

Abstract:

Interleaving/Unrolling and Vectorization are two popular means to optimize applications. While the first one creates multiple copies of the loop body content, the second one focuses on operating on multiple data elements in parallel thanks to SIMD units available in the CPU. In theory, interleaving and vectorization are orthogonal optimizations, one relying on instruction-level parallelism/superscalarity, and the other on data-level parallelism within a single instruction. Modern CPU architectures provide both of these parallelism mechanisms at once, and the combination of vectorization and interleaving is complex, influencing each other due to instruction selection and complexity of underlying hardware, and the programmer often has to rely on the compiler's auto-vectorization.

Based on a large evaluation of 642 loops coming from the literature, this paper demonstrates that significant gains (up to 20%) can be obtained by adapting the LLVM auto-vectorizer to better exploit interleaving and vectorization for a given AArch64 architecture. The proposed approach is flexible and can be easily applied at both loop level or application level. Experiments on 5 mini-apps coming from the HPC realm show similar improvements and demonstrates the co-design potential of the presented approach.

Abstract: https://arxiv.org/abs/2405.11182

PDF: https://arxiv.org/pdf/2405.11182

Section 8, Conclusion:

    In this paper, we quantify the overhead of running a state machine replication system for cloud systems written in a language with GC. To this end, we (1) design from scratch a canonical cloud system—a distributed, consensus-based, linearizable key-values store, (2) implement it in C++, Java, Rust, and Go, (3) evaluate implementations under an update-heavy and read-heavy workloads on AWS under different resource constraints while trying to hit the maximum throughput with a fixed low tail latency. Our results show that even with ample memory, GC has a non-trivial cost, and with limited memory, languages with memory management can achieve an order of magnitude higher throughput than the languages with GC on the same hardware. Our key observation is that if a cloud system is expected to grow to a large volume of users, building the system in a language with manual memory management and thereby paying a higher development cost than using a language with GC may result in a significant cloud cost savings in the long run.