Add Svinval extension.

[kristinbarber]

These changes add the “Svinval” Standard Extension for Fine-Grained
Address-Translation Cache Invalidation, Version 1.0 to the sail-riscv model.

This extension defines five new instructions: SINVAL.VMA, SFENCE.W.INVAL,
SFENCE.INVAL.IR, HINVAL.VVMA, HINVAL.GVMA.

HINVAL.VVMA & HINVAL.GVMA are omitted since they build on the
Hypervisor Extension which is yet to be included in the model.

SFENCE.W.INVAL & SFENCE.INVAL.IR are treated as nops pending integration
of the coherency model (rmem) with sail.

The specification says that SINVAL.VMA behaves just as SFENCE.VMA,
except there are additional ordering constraints with respect to the new
SFENCE.W.INVAL & SFENCE.INVAL.IR instructions. Since these are nops, we
can treat SINVAL.VMA as if it were SFENCE.VMA.

[kristinbarber]

I see this PR is tagged with tgmm-agenda. Has this been reviewed? Can we get an update soon?

[jrtc27]

For one, why is your commit message entirely indented?

[jrtc27]

Suggested change

[jrtc27]

That's not true for rmem? It models memory ordering.

[jrtc27]

These need to be gated on the ISA extension, and should be in their own Svinval file

[jrtc27]

Suggested change

	/* Guarantees that any previous stores already visible to the
	* current RISC-V hart are ordered before subsequent SINVAL.VMA.
	* Can be implemented as a no-op since all memory operations are
	* visible immediately in the current model.*/
	/* Guarantees that any previous stores already visible to the
	* current RISC-V hart are ordered before subsequent SINVAL.VMA.
	* Can be implemented as a no-op since all memory operations are
	* visible immediately in the current model.
	*/

is the current (ugly) style. Definitely needs a space before the */ at least.

(ditto below)

[jrtc27]

I see this PR is tagged with tgmm-agenda. Has this been reviewed? Can we get an update soon?

The TG is dysfunctional; often either code doesn't get reviewed in a timely manner or it gets approved without proper review.

[Alasdair]

Well, this is true in a sense, but the real underlying problem is there is no one person who has both editorial control over the model and sufficient time to dedicate to exercising that control. Everyone involved has other responsibilities. You have to remember that companies like ARM and Intel have teams of engineers dedicated to their formal models, whereas in the RISC-V world there seems to be an interest in having equivalent capabilities but little to no actual investment in making that happen. I don't think these issues are isolated to the formal group.

Note that I'm not a maintainer here, so that's just my personal opinion of the issues involved. I do attend the meetings, so I will make sure that this PR gets brought up - Integrating the current state of the RISC-V model into our concurrency machinery is overdue and has been on my todo list for a while, so having these stubs be in place for me would be useful.

[jrtc27]

Well, this is true in a sense, but the real underlying problem is there is no one person who has both editorial control over the model and sufficient time to dedicate to exercising that control. Everyone involved has other responsibilities. You have to remember that companies like ARM and Intel have teams of engineers dedicated to their formal models, whereas in the RISC-V world there seems to be an interest in having equivalent capabilities but little to no actual investment in making that happen. I don't think these issues are isolated to the formal group.

Yes, this is precisely the cause of the dysfunction. RISC-V as a whole is limited by availability of people with both time and experience simultaneously, but the formal model side is the bottom of the barrel in terms of number of people who are interested and have time to spend on it (whether reviewing or contributing changes); for most companies, they just care about getting their ideas for an extension in, not this weird pesky formal model thing. So yes, there are similar problems on the ISA and non-ISA specifications front, but nowhere near to the degree seen here, and there seems to be zero interest from RISC-V International in fixing this problem, or perhaps even acknowledging it exists in the first place.

[github-actions]

Unit Test Results

712 tests  ±0   712 ✔️ ±0   0s ⏱️ ±0s
    6 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit bc9f38a. ± Comparison against base commit dbea780.

[allenjbaum]

Hmm, as someone familiar with the backlog for arch-test, and all the associated tools it uses, I might disagree with that. Both have the same issues.

…

On Fri, Oct 27, 2023 at 1:31 PM Jessica Clarke ***@***.***> wrote: Well, this is true in a sense, but the real underlying problem is there is no one person who has both editorial control over the model and sufficient time to dedicate to exercising that control. Everyone involved has other responsibilities. You have to remember that companies like ARM and Intel have teams of engineers dedicated to their formal models, whereas in the RISC-V world there seems to be an interest in having equivalent capabilities but little to no actual investment in making that happen. I don't think these issues are isolated to the formal group. Yes, this is precisely the cause of the dysfunction. RISC-V as a whole is limited by availability of people with both time and experience simultaneously, but the formal model side is the bottom of the barrel in terms of number of people who are interested and have time to spend on it (whether reviewing or contributing changes); for most companies, they just care about getting their ideas for an extension in, not this weird pesky formal model thing. So yes, there are similar problems on the ISA and non-ISA specifications front, but nowhere near to the degree seen here, and there seems to be zero interest from RISC-V International in fixing this problem, or perhaps even acknowledging it exists in the first place. — Reply to this email directly, view it on GitHub <#297 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJWVUNVKCQUREQKFWULYBQK35AVCNFSM6AAAAAA34NHZJCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTOOBTGQ3TQNZUGQ> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[jjscheel]

So yes, there are similar problems on the ISA and non-ISA specifications front, but nowhere near to the degree seen here, and there seems to be zero interest from RISC-V International in fixing this problem, or perhaps even acknowledging it exists in the first place.

I can confirm that the gaps in both SAIL and ACT are a regular topic (as @allenjbaum and @billmcspadden-riscv can attest) with the RVI Board for at least the past 3 months. So, while people may not have visibility to these discussions, it's not accurate to portray RVI as having "zero interest".

Additionally, I'd provide a couple additional observations:

1. Foundations operate at a slower pace than stand alone organizations because decisions often require a certain amount of diplomacy and consensus building across organizations. This indeed can be perceived as "zero interest" but time and patience hopefully prove it incorrect.
2. Complicating the challenges here are the need for specialized skills. We cannot and should not think about simply throwing bodies at this. These gaps require folks who have deep ISA skills, language enthusiasts, and software build and test experts who all hopefully know or can learn OCaml.
3. Once we have appropriate skills, it will be up to the existing community to embrace, encourage, tutor and ultimately support the new members. While individual mentoring can be done, comprehensive documentation about development tooling, coding style, community processes and best practices, and technical howto (cookbook) examples is the most effective way to shorten on-boarding and minimize the community impacts of growth.

So, yes, there's improvement needed but I believe lots of people are trying to make it better. It's just going to take time and effort from all of us.

[ptomsich]

Well, this is true in a sense, but the real underlying problem is there is no one person who has both editorial control over the model and sufficient time to dedicate to exercising that control. Everyone involved has other responsibilities. You have to remember that companies like ARM and Intel have teams of engineers dedicated to their formal models, whereas in the RISC-V world there seems to be an interest in having equivalent capabilities but little to no actual investment in making that happen. I don't think these issues are isolated to the formal group.

Yes, this is precisely the cause of the dysfunction. RISC-V as a whole is limited by availability of people with both time and experience simultaneously, but the formal model side is the bottom of the barrel in terms of number of people who are interested and have time to spend on it (whether reviewing or contributing changes); for most companies, they just care about getting their ideas for an extension in, not this weird pesky formal model thing. So yes, there are similar problems on the ISA and non-ISA specifications front, but nowhere near to the degree seen here, and there seems to be zero interest from RISC-V International in fixing this problem, or perhaps even acknowledging it exists in the first place.

I have to sign off for freeze of new extensions on behalf of the Apps & Tools HC. For the last couple months I have been withholding sign-off unless the formal model has at least been submitted as a PR.

Having patches submitted as a PR is not the same as having a positive review — and until we can ensure timely reviews, this would likely cause quite an uproar. However, this has been a useful first step and has been exposing the lack of review and editorial capacity.

[martinberger]

However, this has been a useful first step and has been exposing ...

Thanks. I agree this is very useful. Please stick to that policy.

[martinberger]

I think the PR is good, except for the missing gates.

I don't have time right now to update @kristinbarber's PR, so I'll just attach riscv_insts_svinval.sail as we use it at [company]:

• riscv_insts_svinval.sail.txt

(Sorry for attaching it as a *.txt but Github doesn't seem to let me attach it as *.sail.

@billmcspadden-riscv @jrtc27

[martinberger]

I've added the required gates, and created a new PR at #463