Page MenuHomeFreeBSD
Differential D57812

memory_model(7): create and document pointer provenance
ClosedPublic
Actions

Authored by brooks on Wed, Jun 24, 10:07 AM.
Tags
None
Referenced Files
Unknown Object (File)
Thu, Jun 25, 12:52 AM
Unknown Object (File)
Wed, Jun 24, 8:06 PM
Unknown Object (File)
Wed, Jun 24, 1:52 PM
Unknown Object (File)
Wed, Jun 24, 12:29 PM
Unknown Object (File)
Wed, Jun 24, 10:19 AM
Subscribers
emaste
imp
jrtc27
kib
markj
ziaee

Details

Reviewers
adrian
markj
emaste
kib
Group Reviewers
cheri
Commits
rG1366a87c9cb5: memory_model(7): create and document pointer provenance
Summary

Add a skeleton manpage intended to describe the FreeBSD memory model.

To start with, add documentation of pointer provenance and a cross link
to atomic(9).

Provide some advice on preserving provenance in CHERI and reference
more detailed discussions.

Effort: CHERI upstreaming
Sponsored by: Innovate UK

Diff Detail

Repository
rG FreeBSD src repository
Lint
Lint Not Applicable
Unit
Tests Not Applicable

Event Timeline

There are a very large number of changes, so older changes are hidden. Show Older Changes
emaste added inline comments.Wed, Jun 24, 10:39 AM
share/man/man7/arch.7
245 ↗(On Diff #180516)

Other section headings are title case

246 ↗(On Diff #180516)
249 ↗(On Diff #180516)
261 ↗(On Diff #180516)

Also this makes for a long sentence. The parenthetical statement could just stand alone I think:

subject to monotonically guarantees.
No manipulation of a capability ...

268 ↗(On Diff #180516)
270 ↗(On Diff #180516)
272 ↗(On Diff #180516)
274 ↗(On Diff #180516)

This list mixes grammatical forms; we should consistently use one.

I prefer the way imperative reads in general (i.e., changing the others, not this one) but the introduction to the list would then need to change. Either way they should be consistent.

278 ↗(On Diff #180516)
301 ↗(On Diff #180516)
302 ↗(On Diff #180516)
307 ↗(On Diff #180516)
309 ↗(On Diff #180516)
emaste added inline comments.Wed, Jun 24, 12:21 PM
share/man/man7/arch.7
274 ↗(On Diff #180516)

Further to this, we have two use cases for this information

  • what is pointer provenance?
  • what do I need to do to write correct code?

Pointer provenance in general is a correctness concern (e.g. compiler UB), but the harder requirements in alternate mem* functions are not obvious outside of CHERI. So maybe a section of specific rules:

  • Move pointer values only through pointer types or intptr_t/uintptr_t, never through other integer types.
  • When you copy memory that may contain pointers, use a provenance-preserving copy (memcpy, memmove, copyinptr, copyoutptr); use the _data variants only for raw bytes where you specifically don't want pointers carried along.
  • If you only need the numeric address, use ptraddr_t.

...

brooks updated this revision to Diff 180525.Wed, Jun 24, 12:28 PM

Address feedback from @emaste

Harbormaster completed remote builds in B74198: Diff 180525.Wed, Jun 24, 12:28 PM
brooks marked 14 inline comments as done.Wed, Jun 24, 12:31 PM
brooks added inline comments.
share/man/man7/arch.7
245 ↗(On Diff #180516)

Except "Type sizes" immediately above.

emaste added inline comments.Wed, Jun 24, 12:46 PM
share/man/man7/arch.7
284 ↗(On Diff #180525)
305 ↗(On Diff #180525)
306 ↗(On Diff #180525)
315 ↗(On Diff #180525)
326 ↗(On Diff #180525)
brooks updated this revision to Diff 180526.Wed, Jun 24, 12:53 PM
brooks marked 5 inline comments as done.

Fix more typos

Move out of bounds pointer rule lower.

Harbormaster completed remote builds in B74199: Diff 180526.Wed, Jun 24, 12:53 PM
emaste added inline comments.Wed, Jun 24, 1:11 PM
share/man/man7/arch.7
288 ↗(On Diff #180526)

"direct access" was a bit ambiguous to me, maybe this suggestion is more explicit?

245 ↗(On Diff #180516)

Fair enough, but Endianness and Char Signedness below is title case. If not-title-case is the way we want to go we should subsequently change the others.

markj accepted this revision as: markj.Wed, Jun 24, 1:58 PM
markj added a subscriber: markj.
markj added inline comments.
share/man/man7/arch.7
288 ↗(On Diff #180526)

+1

321 ↗(On Diff #180526)

I guess there's no qsort_data()?

This revision is now accepted and ready to land.Wed, Jun 24, 1:58 PM
brooks added inline comments.Wed, Jun 24, 2:13 PM
share/man/man7/arch.7
321 ↗(On Diff #180526)

It's certainly possible to add one, but I don't think it would have major value.

I mostly added a mention of qsort to point out that it's not just copying that needs to be tweaked. It might be better to drop it and keep that in the cheri(7) phk suggested.

brooks updated this revision to Diff 180531.Wed, Jun 24, 2:16 PM

Clarify alignment requirement somewhat

Drop mention of qsort.

This revision now requires review to proceed.Wed, Jun 24, 2:16 PM
Harbormaster completed remote builds in B74201: Diff 180531.Wed, Jun 24, 2:16 PM
adrian added a comment.Wed, Jun 24, 2:33 PM

Thanks for doing this!

adrian accepted this revision.Wed, Jun 24, 2:35 PM
This revision is now accepted and ready to land.Wed, Jun 24, 2:35 PM
brooks updated this revision to Diff 180537.Wed, Jun 24, 2:51 PM
brooks marked 3 inline comments as done.

Use title case, rebase on D57820

This revision now requires review to proceed.Wed, Jun 24, 2:51 PM
Harbormaster completed remote builds in B74203: Diff 180537.Wed, Jun 24, 2:51 PM
brooks added a parent revision: D57820: arch.7: used title case for .Ss headings.Wed, Jun 24, 2:52 PM
brooks added inline comments.
share/man/man7/arch.7
245 ↗(On Diff #180516)

I've gone and made it somewhat more consistent in D57820. The tree overall is fairly inconsistent on a file-by-file bases with sentence-case, title-case, and capitalize-all-the-things case.

brooks marked 2 inline comments as done.Wed, Jun 24, 2:54 PM
emaste accepted this revision as: emaste.Wed, Jun 24, 2:55 PM
emaste added a subscriber: kib.

LGTM. I do like @kib's suggestion of memory_model(7) or so, and if we're going to do that it makes sense to do so before adding all of the .Xrs elsewhere. But I'm fine as is too.

This revision is now accepted and ready to land.Wed, Jun 24, 2:55 PM
adrian accepted this revision.Wed, Jun 24, 4:04 PM
emaste added inline comments.Wed, Jun 24, 8:11 PM
share/man/man7/arch.7
266 ↗(On Diff #180537)

Maybe "Specifically:" or "To do so:"

306 ↗(On Diff #180537)

Make sense to make these imperative to match the first list maybe?

kib added inline comments.Thu, Jun 25, 12:17 AM
share/man/man7/arch.7
255 ↗(On Diff #180537)

This introductory paragraph is IMO more confusing than the dictionary definition of the 'provenance'.
Could you reuse some text from the standard referenced below, even if not literally?

Esp. useful is the note that provenance is used by optimizers to automatically infer no-aliasing.

brooks updated this revision to Diff 180603.Thu, Jun 25, 10:07 AM

Rework intro text.

Be more direct about when to use copy variants.

This revision now requires review to proceed.Thu, Jun 25, 10:07 AM
Harbormaster completed remote builds in B74233: Diff 180603.Thu, Jun 25, 10:07 AM
brooks marked 3 inline comments as done.Thu, Jun 25, 10:12 AM
brooks retitled this revision from arch.7: discuss pointer provenance to memory_model(7): create and document pointer provenance.Thu, Jun 25, 10:17 AM
brooks edited the summary of this revision. (Show Details)
brooks updated this revision to Diff 180607.Thu, Jun 25, 10:19 AM
brooks edited the summary of this revision. (Show Details)

Move contents to a new memory_model.7

Harbormaster completed remote builds in B74235: Diff 180607.Thu, Jun 25, 10:19 AM
kib added inline comments.Thu, Jun 25, 2:36 PM
share/man/man7/memory_model.7
48

why char * is in parenthesis, but intptr_t's are not?

75

AFAIR 'one past size' is allowed, no?
And, is it requirement for the address at all, or pointers (as distinguished by the text)?

jrtc27 added a subscriber: jrtc27.Thu, Jun 25, 2:41 PM
jrtc27 added inline comments.
share/man/man7/memory_model.7
75

One past the end is allowed, yes. And yes. Should be something like "Avoid manipulating pointers such that they have an address that is neither within the underlying allocation nor one past the end of it."

adrian added inline comments.Thu, Jun 25, 2:46 PM
share/man/man7/memory_model.7
75

Is "one past the end" a CHERI specific thing, or listed in a working group doc proposal for C standard or something else?

jrtc27 added inline comments.Thu, Jun 25, 2:51 PM
share/man/man7/memory_model.7
75

That's an ISO C requirement, and "one past the end" is used in some places of the ISO spec (sometimes also "one past the last element")

brooks updated this revision to Diff 180635.Thu, Jun 25, 4:44 PM

Fix headers. Mention that one past the end is permitted.

Harbormaster completed remote builds in B74260: Diff 180635.Thu, Jun 25, 4:44 PM
brooks marked 4 inline comments as done.Thu, Jun 25, 4:59 PM
brooks added inline comments.
share/man/man7/memory_model.7
48

char * is a pointer type (and usually the one you want to use if you're doing math that doesn't require an integer type). intptr_t and uintptr_t are integer types with the guarantee that you can round-trip a pointer through them.

That being said, I agree this is an awkward construction.

75

I've added a mention of one past the end. I've waffled and not added a mention that de facto C does allow this which is why big CHERI (RV64Y or Morello vs CHERIoT) does allow pointers to go somewhat out of bounds.

brooks marked an inline comment as done.Thu, Jun 25, 5:37 PM
kib accepted this revision.Thu, Jun 25, 10:13 PM
This revision is now accepted and ready to land.Thu, Jun 25, 10:13 PM
emaste accepted this revision as: emaste.Fri, Jun 26, 1:27 AM

LGTM except some small notes

share/man/man7/memory_model.7
17

I presume this is what you meant

25
Closed by commit rG1366a87c9cb5: memory_model(7): create and document pointer provenance (authored by brooks). · Explain WhyFri, Jun 26, 11:26 AM
This revision was automatically updated to reflect the committed changes.
brooks added a commit: rG1366a87c9cb5: memory_model(7): create and document pointer provenance.

Revision Contents
Changeset List

PathSize
share/
man/
man7/
1 line
121 lines

Diff 180695

View Options

share/man/man7/Makefile

Loading...
View Options

share/man/man7/memory_model.7

Loading...