Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[herd] Add variant lse2 which implements the Armv8-A FEAT_LSE2 #670

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

relokin
Copy link
Member

@relokin relokin commented Sep 22, 2023

The new lse2 variant changes the default semantics for pair instructions and ensure that their explicit belong to the same atomicity class.

Note that for now, herd doesn't perform any checks on the alignment of the data locations accessed by the pair instruction.

In addition, it changes the definition of the sca-class relation, to exclude the id relation. This change doesn't make any changes to the model as all uses of sca-class are optional and thefore the id subset of the old sca-class relation is unnecessary.

@jalglave
Copy link
Member

Thanks @relokin this looks good.
Jade

Copy link
Collaborator

@HadrienRenaud HadrienRenaud left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me!

You probably have looked into the case of misaligned accesses where the ASL code says the atomicity is "implementation defined"?

herd/variant.mli Outdated Show resolved Hide resolved
herd/variant.ml Outdated Show resolved Hide resolved
@relokin
Copy link
Member Author

relokin commented Sep 23, 2023

Thank you both for the review!

@relokin
Copy link
Member Author

relokin commented Sep 23, 2023

Looks good to me!

You probably have looked into the case of misaligned accesses where the ASL code says the atomicity is "implementation defined"?

I haven't and with a quick grep I couldn't find it, could you give me a pointer?

@HadrienRenaud
Copy link
Collaborator

Looks good to me!
You probably have looked into the case of misaligned accesses where the ASL code says the atomicity is "implementation defined"?

I haven't and with a quick grep I couldn't find it, could you give me a pointer?

In MemSingle, there is the following case (I don't understand when it is triggered):

        // Misaligned accesses within 16 byte aligned memory but
        // not Normal Cacheable Writeback are Atomic
        atomic = boolean IMPLEMENTATION_DEFINED "FEAT_LSE2: access is atomic";

@relokin
Copy link
Member Author

relokin commented Sep 25, 2023

Looks good to me!
You probably have looked into the case of misaligned accesses where the ASL code says the atomicity is "implementation defined"?

I haven't and with a quick grep I couldn't find it, could you give me a pointer?

In MemSingle, there is the following case (I don't understand when it is triggered):

        // Misaligned accesses within 16 byte aligned memory but
        // not Normal Cacheable Writeback are Atomic
        atomic = boolean IMPLEMENTATION_DEFINED "FEAT_LSE2: access is atomic";

Thank you! Ah yes, I've seen that, I thought you were referring to the asllib code in herdtools.

Not sure, but from what I can gather, it says that the architecture doesn't mandate that the access is single-atomic but an implementation can implement it as atomic.

The new lse2 variant changes the default semantics for pair
instructions and ensure that their explicit belong to the same
atomicity class.

Note that for now, herd doesn't perform any checks on the alignment of
the data locations accessed by the pair instruction.

In addition, it changes the definition of the sca-class relation, to
exclude the id relation. This change doesn't make any changes to the
model as all uses of sca-class are optional and thefore the id subset
of the old sca-class relation is unnecessary.

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
@jalglave
Copy link
Member

hi @relokin is there any reason to hold this off? How can I help to get this in?
Thanks in advance,
Jade

@relokin
Copy link
Member Author

relokin commented Nov 27, 2023

hi @relokin is there any reason to hold this off? How can I help to get this in? Thanks in advance, Jade

Happy to merge this, only one note, if one used -variant lse2, LDP/STP would be single-copy atomic regardless of the alignment of their operand. I think that's ok for now, and we can still merge this.

@jalglave
Copy link
Member

Thanks @relokin would you be able to add a little warning to the user then?
Thanks in advance,
Jade

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants