Skip to content

Instantly share code, notes, and snippets.

View utaal's full-sized avatar

Andrea Lattuada utaal

107 followers · 26 following
View GitHub Profile
@utaal
utaal / verus_pptr_example.rs
Created May 1, 2024 18:25
use vstd::prelude::*;
verus! {
use vstd::ptr::PPtr;
// ** each executable line is preceded by a comment with the equivalent regular rust unsafe code **
fn main() {
// let ptr = std::alloc::alloc(std::alloc::Layout::new:: <u64>()) as *mut u64;
@utaal
utaal / Goals.md
Last active April 13, 2021 19:24
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.

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)
@utaal
utaal / polonius_stdout
Created June 29, 2020 12:42
# 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 April 23, 2020 09:11
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.

Protocol

  • 3 advertising channels;
@utaal
utaal / grant_data_race.rs
Created April 14, 2020 14:04
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
utaal / doop-graph.html
Created May 27, 2019 08:57
Frank's epic doop dataflow
<body>
<style>
body, text {
font-weight: 300;
font-family: "Helvetica Neue", Helvetica, Arial, sans-serf;
font-size: 14px;
}
#graph {
width: 100%;
@utaal
utaal / arrange.py
Last active June 26, 2018 08:53
#!/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,
@utaal
utaal / README.md
Last active June 7, 2018 10:04
@utaal
utaal / mistake.rs
Created October 18, 2017 13:00
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| {
@utaal
utaal / notes.md
Last active June 13, 2017 13:49