Skip to content

[Work in Progress] Enriching Steel's memory model

Jump to bottom Edit New page
John Li edited this page Jun 8, 2021 · 13 revisions

C memory model for Steel

We would like to add support in Steel for:

  • Pointers, including

    • pointers to struct fields 1 2 3 4
    • pointers to subarrays 1
    • fractional permissions
    • custom PCMs (e.g. resource handles, channels)
    • pointer arithmetic on arrays (lower priority, if at all)
      • hard to correctly and usefully model permissions on subtracting a pointer

    and excluding:

    • reading one field of a struct through a pointer to another field
    • pointer arithmetic on non-arrays in general
    • pointers to continguous substructs of a struct

  • Unions, without the ability to write in one field and read out of another

    • if you have a union of two types S and T holding a value of type S, can switch to T by writing to one of T's fields; in that case, cannot read any of T's other fields
      • in this situation, should it be possible to take write-only pointers to uninitialized fields of T?

Aymeric's notes from this morning's meeting

A summary of this morning's discussion.

To design a Steel memory model compatible with C extraction, we are trying to strike a balance between:

  • Expressiveness: The memory model should not restrict the expressiveness of the Steel separation logic. For instance, considering arrays, a user should be able to define/use arrays with custom PCMs, monotonicity, frozen prefixes, ...
  • Genericity: We do not want to multiply libraries and duplicate code. For instance, considering pointers, we should have a unique user-facing abstraction that encapsulates both standard C pointers and field pointers.
  • Simplicity of the extraction: The memory model must be compatible with KreMLin's pattern-matching based extraction. To get there, a metaprogramming preprocessing phase (ideally, through normalization) is possible. Furthermore, the memory model must remain close enough to C to make a meta-argument about the soundness of the extraction.
  • Proposed plan of action:

For now, we want to focus on expressiveness, and gaining experience modeling different C idioms in Steel. In particular, try to model different versions of arrays, structs, and unions. We restrict ourselves to structured programming, in particular, preventing pointer arithmetic on struct fields/unions. While experimenting, John will draft a wiki page with the pros and cons of different approaches. Once we have models we are happy with, we will think about genericity, possibly building upon Denis' preliminary work using a pointer typeclass.

In addition to standard C idioms, it might also be useful to generalize examples/steel/Selectors.PtrLList to lists of arbitrary vprops. It could help with understanding how to do arrays of structs, structs of arrays, ...

  • Additional comments on the current proposal for Steel.Array:

Tahina's proposed design relies on a sequence of references. This gives us a basis for C-like arrays, but could lead to several issues. First, it is unclear how this model would be compatible with user-defined PCMs on the full array (needed for monotonic/frozen-prefix arrays for instance). Second, this model is a bit further from the C standard, which leads to a more hand-wavy extraction soundness argument. An alternative previously proposed by Jonathan and Denis (in the context of structs, but it should be applicable to arrays) was to instead use a reference to a sequence, and to rely on fictional separation logic to model subarray permissions.

In addition to the aforementioned issues, specifying adjacency in the current library is problematic. Low* allowed to take a sub-buffer of a live buffer. In Steel's separation logic, doing this soundly relies on a split into two different arrays. To later merge subarrays into the original array, we need to keep track of the compatibility/adjacency of the subarrays. Currently, our model either allows to:

  • Have split return two new arrays a1, a2 and a pure predicate relating them to the original array (Steel.Array library). This is not C-idiomatic, as a1 corresponds to the same pointer as the original array; we'd only like to return the new array a2 by performing pointer arithmetic.
  • Return only the pointer to the subarray, with a stateful predicate about adjacency operating on the array selectors (Steel.ArrayPtr library). Relying on a stateful predicate seems overkill, and would induce extra reasoning. Combining the best of both worlds currently is an open question.

Pros and cons of various approaches

So far we have the following approaches:

Questions:

  • How invasive of a change is it to switch to fictional separation logic?
  • What are the pros and cons of keeping track of adjacency with a extra pure predicate vs. representing array slices by their delimiting indices? Some discussion at https://github.com/FStarLang/FStar/pull/2309 - If using indices is not so bad for the user, then fictional separation logic may not be necessary
  • Are there applications that require both a PCM on an entire array and the ability to split that array into subarrays?
    • And, is one of the above approaches better than the others in this regard?
  • The arraystruct examples are all for a struct with two fields {x, y}. If there are three fields {x, y, z}, is it possible split {x, y, z} into {x, _, z} and {_, y, _}? - Perhaps unnecessary and instead can just explose explode/recombine operations

To still allow them to write code generic over the various kinds of references they might come up with, we have to ensure that:

  • the "pointer-like" typeclasses is general enough, and
  • our model of structs, arrays, and unions should allow fields/elements with custom PCMs

Denis defines two such typeclasses in Steel.ArrayStruct: rw_pointer for read-write pointers and r_pointer for read-only pointers. If we would like to support uninitialized fields in unions, then it may be useful also to have a typeclass w_pointer of write-only pointers.

Examples of custom PCMs inside arrays, structs, and unions, which we would like to support:

Add a custom footer
Add a custom sidebar
Clone this wiki locally