-
Notifications
You must be signed in to change notification settings - Fork 233
Steel:wishlist
This page is a list of shortcomings of Low*v2 that we absolutely would like to address with STEEL, and in particular the redesign of the user programming model.
- what have we learned from the shortcomings of push/pop frame?
- can we have a more lexical discipline?
- a combinator, e.g.
with_alloca 0ul 12ul (fun b -> ...)where the function receives a permission and must return it - a meta-programmed combinator that takes a list of local variables, e.g.
with_locals [
0ul, 12ul; // local variable int32_t x[12] = 0;
false, 1ul; // local variable bool y[1] = { false };
] (fun x y ->
)
- can we minimize the amount of annotations?
do we stand by the motto that every primitive concept in Low* has to be modeled as an abstract type in F*? do we really want to offer a specific library just for const pointers?
NS, DM, TR, JP:
- this is hard to enforce, probably want the user to state what kind of annotations they expect to see in the generated C code
- probably want a separate language of annotations to be checked by a hook of some sorts, like a tactic
- difficult to figure out what is the right design; for instance one could rely on the user to annotate parameters and local let-bindings with const (the C compiler checks it, or krml) -- or a variant, e.g. user annotates function parameters and kremlin checks const as needed
do we want a primitive library of references? I would advocate arrays of size 1 only -- references should be a special case
kremlin could conceivably have a special treatment for arrays of units to eliminate them
NS, DM, TR, JP:
- PCMs are general and it's hard to settle on any given PCM because they encode layout but also temporal invariants through the use of monotonicity
- it'd be nice to aim for something modular and reusable where someone can combine a shared, canonical layout PCM with a custom PCM for, say, the laws of a state machine, but we're not there yet -- would be nice to investigate
- type class of pointer which is what extraction specializes on, and allows multiple PCMs?
- it seems nice to allow everyone to agree on a distinguished PCM for low-level (concrete) programming while for reasoning over ghost refs could be done with arbitrary PCMs
The array type needs to have its length defined over an abstract module of size_t. size_t will be similar to a machine integer, in that it supports arithmetic operations. However, its maximum value will be unspecified.
Injections from machine integers will be made available, at the expense of generating static asserts in the generated C. We regroup all of the target assumptions in a module called Steel.Target which will expose:
module Steel.Target
val size_at_least16: bool
val size_at_least32: bool
val size_at_least64: bool
val little_endian: bool
These will be defined by hand using compiler macros.
// "Safe" version
val size_of_uint16: x:UInt16.t { Steel.Target.size_at_least16 } -> y:size_t { v y == v x }
// If Kremlin sees any occurrence of this one, it will generate at the beginning of the module: _Static_assert(sizeof size_t >= 2)
val size_of_uint16_assert: x:UInt16.t -> y:size_t { v y == v x }
Oftentimes it's convenient to cast an array of integers to an array of bytes. The C standard comes with a strict aliasing restriction, meaning that we can only cast from uint_n* to char* and back to the exact same uint_n*; furthermore, for proof reasoning purposes, we don't want to allow arbitrary aliasing.
It would be nice to be able to define a magic wand, that takes an array of machine integers, casts it to an array of bytes, and when the user relinquishes the permission for the array of bytes, the permission for the original array is returned to the user.
For its functional specification, this operation would use Steel.Target to figure out whether the encoding is little or big-endian.
We want to revive Tahina's original ArrayStruct experiment. Seeing that we can define things built into the memory model, we will not run into the universe restriction that Tahina encountered earlier, and we should be able to define a type of paths to navigate a flat layout.
There are some C standard restrictions to be aware:
- no empty structs or unions (TBD -- most compilers actually accept them)
- non-zero arrays
For the latter point, there is actually a C feature where one can have this:
struct header {
size_t len;
char data[0];
} header_s;
char *tagged_array = malloc(sizeof header_s + MY_LEN);
((header_s *)tagged_array)->len = MY_LEN;
it would be really nice in terms of expressive power if we could model this with a magic wand.
- https://en.wikipedia.org/wiki/Read-copy-update -- a primitive used pervasively in the linux kernel that would also be very useful for our userland implementation
- spinlocks, semaphores and threads: what is an API that is compilable to C?
- underlying data structure (e.g. pthread_t) is by-address
- passing data to initial thread creation requires the use of void* and cast; time to write Steel.Dyn? any way to make this safe?
- shall we aim for generality (compiles to both windows & unix) or target one specific API (e.g. pthreads) and rely on winpthreads?
discussion:
- would be nice to enforce that the user hoists the closures themselves at the top-level, and we can probably reveal in Steel that the closures receive some heap-allocated data
- no surprises
- kremlin will transform a polymorphic fork-join into pthread_create along with suitable casts to void*
- user-facing API might need to be changed to reflect the thread handle as a pointer to a resource in memory
a custom static allocator for embedded devices, where the outer allocator "owns" the unused slots + bookkeeping data at the beginning of each block, and client "owns" the payload of each allocated block
tricky issues of splitting ownership within a given struct
There should be a null pointer value which has length 0, but also allow for other arrays (for instance splitted arrays) to have length 0. There should not be a lemma saying that any array of size 0 is the null pointer. Null pointer and other arrays of size 0 should be live (they should be in the ressource context) but you can only sub them, no indexing or update
The following situations are naturally encoded into magic wands:
- when you split an array, same thing it should give you the
recombinablepredicate as a magic wand, so that gluing back can just be an application of the magic wand rule - same for sharing permissions. However this would pollute the ressource context with a lot of magic wand predicates, so we might want to do this a logical predicates in the refinements.
For instance you can view a struct as one reference to the whole struct or have a big star of all the fields of the struct. A tactic could do automatic recombining/exploding of the struct depending on what's expected. See heuristics of Mezzo to define a set of tactics to automate common pattern.
Objective => define a limited subset of things where there is very high automation support.