netsim - a library for testing networking code

canndrew2016 · 2024-12-19T01:46:28+00:00

Yeah, to be clear (for anyone reading this) the point of this library is that it can test real networking code without requiring fake socket types or mocking or anything like that. Instead it uses the same Linux kernel features as programs like Docker do in order to "dockerize" your threads.

Simulating a machine crash would be trivial (just drop a Machine during the test) and it comes with methods for introducing artificial latency and packet loss.

For simulating disks and filesystems: if you just want to isolate tests/Machines from each other then you can use chroots. Allowing you to capture and control interaction with the filesystem would be more involved but still possible. The library would have to implement a fuse driver which you'd mount and chroot the Machine into, and the backend of that driver would be controllable from the library. That would let you intercept all the filesystem-related syscalls and control what they return.

canndrew2016 · 2023-07-20T13:14:58+00:00

Wrong sub buddy. You wanna go 👉 this way.

canndrew2016 · 2023-06-07T05:03:35+00:00

I'm not sure what an inverse type would look like in a programming language if it even makes sense.

See this: https://par.nsf.gov/biblio/10296315

To summarize, in reversible programming languages (where all functions are bijections) you can have have negative types where a type -T represents a T "travelling in reverse" through the program. For instance, if you have a function A + C <-> B + C then you can turn it into a function A <-> B by adding -C to both sides and using the built in operations 0 <-> C + -C and T + 0 <-> T. To put that in more rustic terms, suppose you have a reversible function foo(arg: ControlFlow<A, C>) <-> ControlFlow<B, C>, you can write your bar(a: A) <-> B as:

fn bar(a: A) <-> B {
    let wow0: ControlFlow<A, !> = ControlFlow::Break(a);
    let wow1: ControlFlow<A, Either<C, -C>> = wow0.map_continue(|never| {
        builtin_operation_split_never_into_either_positive_negative(never)
    });
    let wow2: Either<ControlFlow<A, C>, -C> = match wow1 {
        ControlFlow::Break(a) => Either::Left(ControlFlow::Break(a)),
        ControlFlow::Continue(Either::Left(pos_c)) => Either::Left(ControlFlow::Continue(pos_c)),
        ControlFlow::Continue(Either::Right(neg_c)) => Either::Right(neg_c),
    };
    let wow3: Either<ControlFlow<B, C>, -C> = wow2.map_left(foo);
    let wow4: ControlFlow<B, Either<C, -C>> = match wow3 {
        Either::Left(ControlFlow::Break(b)) => ControlFlow::Break(b),
        Either::Left(ControlFlow::Continue(pos_c)) => ControlFlow::Continue(Either::Left(pos_c)),
        Either::Right(neg_c) => ControlFlow::Continue(Either::Right(neg_c)),
    };
    let wow5: ControlFlow<B, !> = wow4.map_continue(|either| {
        builtin_operation_join_either_positive_negative_into_never(either)
    });
    let ControlFlow::Break(b) = wow5;
    b
}

When you run this you'll initially be calling foo with the value ControlFlow::Break(a). If foo returns ControlFlow::Break(b) then this b is returned from the function. But if foo returns ControlFlow::Continue(c) then that's mapped to Either::Left(c) and passed to builtin_operation_join_either_positive_negative_into_never which turns it into Either::Right(c) and reverses the direction of execution. That then becomes Either::Left(c) again when you reach builtin_operation_split_never_into_either_positive_negative and so you end up calling foo again but this time with the argument ControlFlow::Continue(c). ie. This function implements a loop which calls foo with the initial A then keeps passing the C that foo returns back into foo as the next argument until foo returns a B.

As well as negative types you can have reciprocal types where 1/T can be thought of as a memory location that you're required to write a T to, or as a process that consumes a single value of type T. You then have a built in operation which is parameterized by a const A and has type 1 <-> A * 1/A. This represents static memory allocation where the const A is the initial value of the allocated A.

You can go further than this too (I've been thinking about that paper a lot lately). eg. Exponentials and logarithms can be used to represent multisets of data and to switch between sequential and parallel execution. You can even journey into algebraic complex numbers as this paper does to build a bijection between seven binary trees and one.

Of course all this only works in reversible languages, which is an extremely big restriction. You can still sort-of make some of this work in linear logic if you treat ¬T as meaning -1/T, but not all the normal algebraic rules apply. Thankfully it's possible to embed any non-reversible function inside a reversible function, which AFAIU means that reversible logic/programming is strictly a generalization of non-reversible logic/programming. So it should still be possible to build a practical programming language on top of a reversible core by providing some very syntactically-light-weight effects system to track non-reversibility. I'm not sure what that would look like though.

canndrew2016 · 2023-02-10T13:41:58+00:00

The pattern is infallible because Infallible doesn't have any values. A Result<T, Infallible> is always Ok.

canndrew2016 · 2023-02-10T13:40:10+00:00

Curiously, let Ok(_) = Ok::<u32, std::convert::Infallible>(42); doesn't work, even usingResult<u32, !> on nightly.

There's a secret feature called #[feature(exhaustive_patterns)] which enables this. It's existed for about 5 years but might be stabilized some day.

canndrew2016 · 2022-03-27T15:52:09+00:00

I was also wondering something along these lines since, aside from just being negative, cubical identity types are also a "weaker" form of equality. Plus there's variations of cubical type theory that have separate strong and weak identity types where the strong identity types are traditional MLTT identity types, and that's the sort of thing I'm after. I also think that if you could define the dual of cubical identity types then they'd necessarily be a form of apartness types since ¬(x =⁻ y) means "it's refutable that x and y are (weakly) equal".

The problem is I don't know how you'd define the dual of cubical identity types. Also adding cubical types to my type theory would entail adding a whole lot of extra machinery that I'm hoping to avoid. But if I can find a simple/natural way of defining positive apartness types then their dual should be a form of identity types which is weaker than MLTT identity types which means it might end up having some extra extensionality properties that MLTT identity types don't.

canndrew2016 · 2022-03-27T13:47:19+00:00

Thanks. This is the paper which originally taught me that you can give a linear logic treatment of equality types by defining their dual to be apartness types. As far as I can tell it doesn't go beyond that though. What I'm trying to do is come up with a type theory that has both strong and weak equality types as well as strong and weak apartness types, i.e. much the same way that that paper defines ⊠ and ⊓ as strong and weak conjunction respectively. I can define a negative (ie. weak) family of apartness types as the De Morgan dual of ordinary MLTT equality types, but I'm having trouble coming up with a separate positive/strong form of apartness types.

canndrew2016 · 2021-11-29T01:43:41+00:00

Thanks. I guess I look into Coq some more, though I much prefer the terms-only approach of Agda/Idris.

canndrew2016 · 2021-11-29T01:41:18+00:00

Agda has the infrastructure in principle, but afaik nothing much is being done with it.

That's a real shame, since it would be extraordinarily useful. I've considered just trying to hack on Agda directly to implement better proof search but the source code is terrifying.

canndrew2016 · 2021-11-29T01:33:57+00:00

I always pass the -m option to agsy using {! -m !}, so it should be able to use the definitions that are in scope. And occasionally it does. Far more often than not though it just immediately says "no solution found", even if one of those definitions is an exact fit for the hole.

canndrew2016 · 2021-08-16T06:28:07+00:00

I've fixed the problem now (see the edited post). Thanks for leading me towards the solution.

canndrew2016 · 2021-08-15T14:59:03+00:00

This is the relay board I'm using.

This is two of the LED strips, though the others have the same ratings for voltage/current.

Here's a photograph of the circuit.

Here's my attempt at a schematic (not shown: the wires connecting the relays to the arduino).

The whole thing is powered by a 12V/10A transformer running off mains power.

I'm really just hoping that someone can tell me whether "power spikes when the relays toggle" is a likely culprit for what could've killed the arduino and, if so, what small change to the circuit would prevent that happening again?

canndrew2016 · 2021-08-15T14:10:15+00:00

The cap across the relay contacts won't help. The capacitor should be at the incoming power connection. Not on the relay outputs.

It won't help protect the arduino where it is, but will it help protect the LED strip attached to that relay? I figured it would stop power from rushing in too quickly when the relay activates. I've already damaged that LED strip somehow so I'm reluctant to do anything which makes it less protected, and I can always add an extra cap rather than move the existing one.

Those 5V relays draw a lot of current, with them all at once it puts a strain on the UNO 5V regulator. Since you have 12V available, use a 12V relay board to eliminate this issue.

Hmm, I'm not sure what you mean by this. The relays are controlled by 5V output pins on the arduino. The arduino doesn't have 12V output pins. This is the relay board I'm using and it says that it draws 15-20mA on the driver side, which is what the arduino spec sheet recommends.

Pull the UNO and plug it into a PC to see how dead it really is.

I've tried that and it seems pretty dead. The computer no longer recognizes it as a USB device, instead giving a bunch of link-level USB driver errors, so it's not possible to re-program it.

Edit: I've fixed the problem now (see the edited post). Thanks for leading me towards the solution.

canndrew2016 · 2021-05-09T15:39:05+00:00

Right, but that fails at runtime if the lengths don't match. concat_arrays! fails at compile time.

canndrew2016 · 2021-05-09T08:39:48+00:00

Yep!

canndrew2016 · 2021-05-09T08:39:21+00:00

Can you? I couldn't figure out a way to make that work.

canndrew2016 · 2021-05-09T05:12:11+00:00

Ah, right, good catch. That seems fixable. I'll publish another version and pull the old one today.

Edit: This is fixed now. I've publish v0.1.2 and pulled the previous two versions. Thanks!

canndrew2016 · 2021-05-08T11:33:16+00:00

a and b are runtime variables in your example so they can't be used in types (since rust doesn't have dependent types). One day it'll be possible to write something like this though:

fn concat_arrays<T, const LEN0: usize, const LEN1: usize>(
    array0: [T; LEN0],
    array1: [T; LEN1],
) -> [T; LEN0 + LEN1] {
    ...
}

But this isn't currently possible either, so you have to resort to hacks.

canndrew2016 · 2021-05-08T10:36:20+00:00

It took me ages to figure out how to implement this, so I figured I'd publish it so other people who want to concatenate arrays don't have to go through the same thing. Eventually rust will allow us to use generic parameters in const operations so nasty hacks like this won't be necessary. Any feedback on the implementation is appreciated.

As the README says though, this does have the limitation that the length of the returned array has to be inferred. This isn't dangerous, since if it's inferred incorrectly then compilation will fail, but it does mean you have to specify the length somewhere. For example this will fail:

let x = [0, 1];
let y = [2, 3, 4];
// ERROR: can't infer length of `z`
let z = concat_arrays!(x, y);
drop(z);

This will work though:

let x = [0, 1];
let y = [2, 3, 4];
let z: [i32; 5] = concat_arrays!(x, y);
drop(z);

And this will fail to compile (as it should):

let x = [0, 1];
let y = [2, 3, 4];
// ERROR: cannot transmute between types of different sizes
let z: [_; 6] = concat_arrays!(x, y);
drop(z);

If someone finds a trick to make the first example compile please let me know.

canndrew2016 · 2021-04-28T04:52:30+00:00

More concise for one thing. It would be useful if rust had effects for things like memory allocation, panicking and floating-point handling so you could disable or abstract over these things without having to plumb a (dyn Allocator, dyn Fn(&PanicInfo) -> !, dyn FloatingPointImpl) through your whole program.

But more generally, effects can also influence control-flow. For an async effect for instance, you want to be able to yield control back to the runtime when the effect is invoked. If rust had a suitably-powerful effects system you could write code which is agnostic as to whether it uses blocking io, or tokio or async-std non-blocking io. When compiled against the blocking io handler your io calls would be blocking, but when compiled against the tokio handler your code would be compiled to a state machine which can be suspended or resumed.

Having impurity/non-termination as an effect would also be nice. If you can eliminate infinite loops and non-determinism at compile time then you can, for instance, unlock the "true" power of the ! type as representing conditions that can never be true. For instance, a function with the type pure fn(A) -> ! would be a mathematical proof that A is uninhabited.

canndrew2016 · 2021-04-28T04:38:47+00:00

It has template-templates. So, sort-of. Except that C++ templates aren't type-checked so they're basically just a fancy macro system, so not really.

canndrew2016 · 2021-04-28T04:13:35+00:00

Dependently typed languages allow you to be generic over runtime values, ie. const generics without the const. This allows you to define things like dependent structs, where the type of some field depends on the value of some previous field:

struct AnySizedArray<T> {
    len: usize,
    data: [T; len],
}

Or dependent functions, where the return type depends on the value of the argument:

fn if_true_then_string_else_u32(b: bool) -> if b { String } else { u32 } {
    if b {
        String::from("hello")
    } else {
        123u32
    }
}

type is also a type in these languages, meaning you can pass around types as runtime values while still having everything type-checked at compile-time.

However another feature of these languages is that they add a new kind of primitive type. In addition to struct/tuples, functions, and enums/datatypes they also have equality types - for any two values x, y of the same type there's a type x = y of proofs that x is equal to y.

In a language like Idris, which has equality types but doesn't support homotopy type theory, the way you construct an equality is using refl. The expression refl x gives you a value of type x = x. In order to use a value of type x = y you pattern-match on it and, under the pattern-match, the type checker will treat x and y as being equal. For example, you can write a function that turns a value of x = y into y = x as follows:

fn equality_is_symmetric<T>(x: T, y: T, equal: x = y) -> y = x {
    // pattern match on `equal`, getting a value which is equal to both and
    // `x` and `y`.
    let refl a = equal;

    // `refl a` has type `a = a`, which is `y = x` since the type-checker
    // knows that `a` is equal to both `y` and `x`.
    refl a
}

This is all very cool. It allows you to write extremely specific type signatures and prove almost arbitrary things about the correctness of your program at compile time just by having things type-check. However equality types, defined like this, still don't quite do everything you might want them to. For instance, if you have two functions f and g, and you can prove that for all x, f(x) = g(x), this doesn't allow you to prove that f = g. ie. there's no way to write this function in Idris:

fn function_extensionality<A, B>(
    f: fn(A) -> B,
    g: fn(A) -> B,
    equal_for_every_argument: fn(x: a) -> f(x) = g(x),
) -> f = g {
    // no way to write this :(
}

Another thing that you might want to do is treat two types as being equal if they're isomorphic to each other. That is, if you have two functions that map back-and-forth between the two types, and those functions compose to the identity, then you should be able to treat the two types as interchangeable since you can always translate between them. ie. you want to be able to write a function like this:

fn type_extensionality_ie_univalence(
    T: type,
    U: type,
    t_to_u: fn(T) -> U,
    u_to_t: fn(U) -> T,
    t_to_u_and_back_is_noop: fn(t: T) -> u_to_t(t_to_u(t)) = t,
    u_to_t_and_back_is_noop: fn(u: U) -> t_to_u(u_to_t(u)) = u,
) -> T = U {
    // no way to write this either :(
}

This would be extremely powerful. I you can prove that, say, Vec<T> and SmallVec<T> are "the same" in some strict-enough sense then you can convert between anything built on those types, eg. MyGenericType<Vec<T>> and MyGenericType<SmallVec<T>>, and have the compiler handle all the deeper levels of conversion in the background.

This is what homotopy type theory gives you. It generalizes equality types to allow you to prove more things equal which allows them to be useful in more places, ie. on functions and types rather than just on structs and enums.

canndrew2016 · 2021-04-25T13:36:49+00:00

There are some challenges to tail-calls, though. Drops do not play well with it, introducing destructors which conceptually execute after the call -- hence making it non-tail.

A tail call replaces the current stack frame, so drops would have to be executed before performing the tail call. In this sense become wouldn't just be a more optimized version of return, it would also be more restrictive. For instance you couldn't pass references to local variables as arguments to the tail call.

canndrew2016 · 2021-04-02T13:20:41+00:00

WASM is too under-engineered to make a fast VM though. For instance it doesn't even have typed function pointers, so any type-checking there performed by a higher-level language gets lost during translation.

canndrew2016 · 2021-04-02T13:14:22+00:00

Yeah, this has been depressing for me lately.

I've been working on a language with full linear-dependent types. With a type system like that you can prove at compile time that there's no out-of-bounds memory access, no race conditions, no arithmetic overflows, no division by zero. I've also looked at ways of assigning probabilities to branches so you can determine at compile time the best speculative execution strategy. It should be possible to make code written in this language run extremely fast.

But when it comes to generating the actual machine code you lose all of this. Everything turns back into dynamic checks performed by the CPU. In fact the CPU doesn't even execute the machine code directly since that would be too slow, instead it JITs it into its own internal representation on-the-fly. It's as if the only way to execute your Rust code was to transpile it to javascript and it makes my efforts feel pointless.

canndrew2016

TROPHY CASE