Skip to content

Instantly share code, notes, and snippets.


Andrea Lattuada utaal

View GitHub Profile
utaal /
Last active Apr 13, 2021
iron language design

This fork of Rust is for developing an experimental verification framework for Rust-like code. The main goal is to verify full functional correctness of low-level systems code, building on ideas from existing verification frameworks like Dafny, Boogie, F*, VCC, Prusti, Cogent, Coq, and Isabelle/HOL.


  • provide a pure mathematical language for expressing specifications (like Dafny, F*, Coq, Isabelle/HOL)
  • provide a mathematical language for expressing proofs (like Dafny, F*, Coq, Isabelle/HOL) based exclusively on classical logic (like Dafny)
  • provide a low-level, imperative language for expressing executable code (like VCC), based on Rust (like Prusti)
View polonius_stdout
# errors
# move_errors
move_errors "Mid(bb2[4])" "mp1"
# subset_errors
# restricts
# restricts_anywhere
# origin_live_on_entry
origin_live_on_entry "Start(bb0[0])" "\'_#0r"
origin_live_on_entry "Start(bb0[0])" "\'_#1r"
origin_live_on_entry "Mid(bb0[0])" "\'_#0r"
utaal /
Last active Apr 23, 2020
BLE advertisement frame successful exchange rate in scenarios with many advertising devices

This is based on my partial knowledge of radio networks, and on very incomplete knowledge of the BLE stack.

AFAIK BLE scans in short intervals on one of 3 channels. With >50 devices in advertisement mode it may be hard to get non-colliding frames to the receiver.

  • I don’t think Bluetooth LE was designed to have hundreds of devices in discoverable mode sending out garbage identity frames.
  • Increasing the radio wake time may not be a solution either because you end up with flat batteries too quickly.


  • 3 advertising channels;
utaal /
Created Apr 14, 2020
spsc-bip-buffer potential data race
fn grant_data_race() {
for i in 0..128 {
let (mut writer, mut reader) = bip_buffer_from(vec![0u8; 16].into_boxed_slice());
let mut reservation = writer.reserve(8);
let sender = std::thread::spawn(move || {
writer.reserve(8).as_mut().expect("reserve").copy_from_slice(&[10, 11, 12, 13, 14, 15, 16, i]);
reservation.as_mut().expect("reserve").copy_from_slice(&[1, 2, 3, 4, 5, 6, 7, 8]);
let receiver = std::thread::spawn(move || {
utaal / doop-graph.html
Created May 27, 2019
Frank's epic doop dataflow
View doop-graph.html
body, text {
font-weight: 300;
font-family: "Helvetica Neue", Helvetica, Arial, sans-serf;
font-size: 14px;
#graph {
width: 100%;
#!/usr/bin/env python3
import experiments
def experiment_setup(experiment_name, n, w, **config):
return "{}/{}_n={}_w={}_{}".format(
extern crate timely;
use std::rc::Rc;
use std::cell::RefCell;
use timely::dataflow::InputHandle;
use timely::dataflow::operators::{Input, Exchange, Inspect, Probe, Map};
fn main() {
// initializes and runs a timely dataflow.
timely::execute_from_args(std::env::args(), |worker| {
View ADT.scala
sealed abstract trait ADT
case object One extends ADT
case object Two extends ADT