[crac] RFR: 8373687: [CRaC] Add metrics through jcmd [v7]

[Radim Vansa]

On Tue, 23 Dec 2025 09:47:50 GMT, Radim Vansa <rvansa at openjdk.org> wrote:

>> Enable user adding custom metrics (and labels) through jcmd JDK.checkpoint command, e.g. using
>> 
>> jcmd <pid> JDK.checkpoint metrics=foo=123,bar=0.456
>
> Radim Vansa has updated the pull request incrementally with one additional commit since the last revision:
> 
>   Second round

One of the things that might need some refinement is naming things 'score' vs. 'metric'. When I speak about score, I mean one final value calculated from the individual metrics. But it can also mean the process of calculating the score (and that's why the `Score` class) - but then I see that the `Score.setScore()` method should be `Score.setMetric()` (this is still not exposed to user code so we have a chance to revise this).

-------------

PR Comment: https://git.openjdk.org/crac/pull/281#issuecomment-3685974864