Relation between sref and sloc

[hernanponcedeleon]

I am trying to understand if the property sref <= sloc holds (where <= means subset of) and thus having sloc & sref in the definition of mutordatom is redundant.

If I think of sref and sloc as virtual an physical memory, I think the property should hold. However, it seems that on the device, sref can be other things. Thus, I'm not completely sure if the property should also hold for those cases.

[jeffbolznv]

Hi,

You should think of the reference as being the descriptor used to access a range of memory, rather than being specific to a memory location. So from that point of view, it's clear that sref is not a subset of sloc. For example, you could use a uniform buffer and a storage buffer to access the same location.

There's a change in progress in the Vulkan spec to clarify the definition of reference, which hopefully will make this more clear.

[hernanponcedeleon]

I take as an outcome that the inclusion holds (and thus sloc & sref in the definition of mutordatom is redundant; there are quite a few redundancies in the formal model).

However, your example confused me: the uniform buffer and the storage buffer would be different references (thus their accesses won't be in sref), but since the descriptor is about the same location, they would be in sloc.

Will the change in the spec have any impact in the formal model? Or is it just a clarification on the definition?

[jeffbolznv]

I take as an outcome that the inclusion holds

Why do you say that? I was saying that the inclusion doesn't hold. A reference is more like a descriptor, spanning multiple memory locations. And a memory location can be used with multiple distinct references.

Will the change in the spec have any impact in the formal model? Or is it just a clarification on the definition?

Just a clarification of what a reference is in Vulkan. No change to the formal model.

[hernanponcedeleon]

Why do you say that?

Because you wrote "So from that point of view, it's clear that sref is a subset of sloc."

Imagine you have something like this

// Variable definition
location x
reference y (alias to x)
// Program
NEWTHREAD
e1: st.atom.scopedev.sc0 x = 1
e2: st.atom.scopedev.sc0 y = 1
NEWTHREAD
e3: st.atom.scopedev.sc0 x = 1
e4: st.atom.scopedev.sc0 y = 1

I would definitely expect (a) sref(e2, e4) and (b) sloc(e1,e3) and others ...

My question is: can we infer from (a) that sloc(e2,e4) holds?

[jeffbolznv]

My apologies! I meant to say that it's not a subset. Sorry for the confusion, I'll edit the comment.

In your example, if you say y is an alias to x, then aren't you implicitly assuming they're the same location?

[hernanponcedeleon]

In your example, if you say y is an alias to x, then aren't you implicitly assuming they're the same location?

This example fits in what I initially wrote about seeing sref as a relation between access using virtual memory and sloc as a relation between accesses using physical memory . It might not be the best example for what I am trying to understand because the inclusion sref <= sloc holds.

Here is another example where I expect both sref(e1,e2) and sloc(e1,e2) and thus the inclusion to hold.

// Variable definition
location x
reference y (alias to x)
reference z (alias to x)
// Program
NEWTHREAD
e1: st.atom.scopedev.sc0 y = 1
NEWTHREAD
e2: st.atom.scopedev.sc0 z = 1

What I am missing is an example where sref(e1,e2) but ~sloc(e1,e2).

// Variable definition
location x
location w
reference y (alias to x)
reference z (alias to w)
// Program
NEWTHREAD
e1: st.atom.scopedev.sc0 y = 1
NEWTHREAD
e2: st.atom.scopedev.sc0 z = 1

Here definitely ~sloc(e1,e2). Can you explain a situation where the y,z references/descriptors would be included in sref?

[jeffbolznv]

There's nothing in the model about sref being related to virtual memory. It reflects what descriptor is used to access memory, and descriptors span a range of memory. So you can have two accesses that use the same reference (descriptor) but distinct memory locations within the span of that descriptor.

[hernanponcedeleon]

The last comment was useful, and I think I am starting to understand this.

Is the following correct? I can have two instructions accessing the same buffer (reference) and thus they are in sref. However, the buffer is a range of memory and if they are effectively accessing different locations (let say the front and the back for a non-empty buffer), then they are not in sloc.

[jeffbolznv]

Yes, that's pretty much correct. But to nitpick a bit - just being the same buffer isn't necessarily the same reference, it needs to be the same buffer/offset/range which together fully define the descriptor and in turn the reference.

[hernanponcedeleon]

But wouldn't the offset/range tell you precisely which location you end up accessing? Or could still be the case that the same buffer/offset/range (i.e., reference) access two different locations?

[jeffbolznv]

The same buffer/offset/range can be used to access multiple locations within that range.

[hernanponcedeleon]

Great. This clarifies it for me. Thanks @jeffbolznv for bearing with me 😅

[hernanponcedeleon]

@jeffbolznv it seems that even if sref is not guaranteed to be a subset of sloc, the litmus parser enforces this.

The initial value of pgmsloc at line 573 is pgmsref, thus the inclusion always holds between them. sloc and sref are derived respectively from them as

sloc = ^(rai[pgmsloc]) + stor[R+W]
sref = ^(rai[pgmsref]) + stor[R+W]

so I think the inclusion also holds here.