Skip to content

Instantly share code, notes, and snippets.

Avatar

Andrea Lattuada utaal

View GitHub Profile
@utaal
utaal / Goals.md
Last active Apr 13, 2021
iron language design
View Goals.md

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.

Goals:

  • 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
utaal / ble_frame_collisions.md
Last active Apr 23, 2020
BLE advertisement frame successful exchange rate in scenarios with many advertising devices
View ble_frame_collisions.md

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.

Protocol

  • 3 advertising channels;
@utaal
utaal / grant_data_race.rs
Created Apr 14, 2020
spsc-bip-buffer potential data race
View grant_data_race.rs
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
utaal / doop-graph.html
Created May 27, 2019
Frank's epic doop dataflow
View doop-graph.html
<body>
<style>
body, text {
font-weight: 300;
font-family: "Helvetica Neue", Helvetica, Arial, sans-serf;
font-size: 14px;
}
#graph {
width: 100%;
View arrange.py
#!/usr/bin/env python3
import experiments
def experiment_setup(experiment_name, n, w, **config):
experiments.ensuredir(experiment_name)
return "{}/{}_n={}_w={}_{}".format(
experiments.experdir(experiment_name),
experiment_name,
n,
View README.md
View mistake.rs
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