Skip to content

Instantly share code, notes, and snippets.

#include <stdatomic.h>
#include <pthread.h>
#include <stdio.h>
struct {
const char* _Atomic text[2];
char pad1[128];
int _Atomic flag;
int _Atomic junk;
} msg;
module CCEqual = struct
let physical = Stdlib.( == )
end
module CCHeap : sig
(*
Copyright (c) 2013, Simon Cruanes
All rights reserved.
@stedolan
stedolan / perf.c
Last active October 29, 2025 16:41
#include <linux/perf_event.h>
#include <linux/hw_breakpoint.h>
#include <sys/syscall.h>
#include <unistd.h>
#include <stdio.h>
#include <errno.h>
#include <sys/mman.h>
#include <stdint.h>
#include <assert.h>
#include <x86intrin.h>
(* An implementation of (part of) the lazy data structure of:
First-Order Laziness
Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley
ICFP 2025
Requires OCaml 5.2+ / OxCaml *)
module type LazyS = sig
type _ repr
let enable_hugepages () =
let ch = open_in "/proc/self/maps" in
let module Syscall = struct
external madvise : (int64[@unboxed]) -> (int64[@unboxed]) -> (int[@untagged]) -> (int[@untagged]) =
"unimplemented" "madvise"
end in
try
while true do
Scanf.sscanf (input_line ch) "%Lx-%Lx %s %Lx %x:%x %Ld %s"
(fun start_addr end_addr perms offset devmaj devmin inode path ->

Generating good code for bitfields

Here's a definition of the packed 16-bit RGB565 pixel format as a C struct:

typedef struct { unsigned r : 5, g : 6, b : 5; } pixel;

and a couple of functions that operate on it:

let table = Array.init 10_000 (fun _ -> Bytes.make 1_000 'a')
let writes =
Option.map bool_of_string (Sys.getenv_opt "WRITES")
|> Option.value ~default:false
let[@inline never] f () =
List.init (Array.length table) (fun i ->
let buf = table.(i) in
if writes then table.(i) <- buf;
{-# LANGUAGE GADTs #-}
-- nontermination without any recursion, even in types
-- possible because of impredicativity + injectivity
-- based on https://gist.github.com/leodemoura/0c88341bb585bf9a72e6
-- see also https://github.com/idris-lang/Idris-dev/issues/3687
data False
data I (f :: * -> *) where
let promotion_rate = 50
let collection_rate = 30
let ballast_mb = 100
let iters_m = 50
let rand =
let counter = ref 43928071 in
fun () ->
let n = !counter in
counter := n * 454339144066433781 + 1;
module GenericTrees where
open import Agda.Builtin.String
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Primitive
variable l : Level
-- Products and sums