Concurrency-safe history mechanism proposal (POC)

[robin-aws]

Not intended to be merged, just showing the difference between how History is currently generated and used and how I'd like to refactor it: TestModels/HistoryBefore, particularly SimpleStringImplTest.dfy, shows the pattern of assertions currently supported, and the same test under TestModels/HistoryAfter shows the equivalent after refactoring. I force-added the generated Dafny code so you can explicitly see what gets generated and how I propose to change the code generation logic (by manually editing it after generating it in the HistoryAfter copy).

The proposed change is to make History a locally-passed value instead of a constant on clients themselves. It also uses classes implementing a marker Event trait instead of datatypes, so that the history can be a heterogeneous sequence of events across multiple operations or even clients, instead of a set of independent histories for each operation.

There are a number of advantages to this style:

1. The shared per-client History is not morally concurrency-safe: Dafny is currently proving assertions such as Seq.Last(client.History.GetString).input.value == <what the code above just provided>, but since the client is used by multiple concurrent executions this isn't actually true: other parallel calls could easily have occurred to add more events!
2. The specification of each operation gets slightly simpler, because there isn't the same need to track both Modifies and History separately. It is also compatible with the upcoming support for verifying the {:concurrent} attribute, since the history is no longer shared mutable state across concurrent executions, so it doesn't have to be included in reads or modifies clauses.
3. By using a single history across all clients and operations, it is possible to be more precise about the ordering between different calls, as shown by the third test in HistoryAfter.

The main disadvantage is that by using classes (the only type that can currently extend traits) instead of datatypes to represent call events, the code gets a fair bit more verbose. The helper WasNthLastWith predicate on each event type helps quite a bit, but I'm also open to suggestion on naming and structure.

I've made no effort to hook this temporary structure up in CI, but make verify succeeds on both models at least.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[robin-aws]

Comparing the generated Dafny before and after should help in understanding the proposed code generation changes. Unfortunately I don't see an easy way to get a nice diff of unrelated files on GitHub.

% diff HistoryBefore/Model/SimpleTypesSmithyStringTypes.dfy HistoryAfter/Model/SimpleTypesSmithyStringTypes.dfy 
9a10,11
>  import opened Histories
> 
24,28c26,46
<  class ISimpleTypesStringClientCallHistory {
<  ghost constructor() {
<  GetString := [];
<  GetStringSingleValue := [];
<  GetStringUTF8 := [];
---
> 
> class GetStringEvent extends Event {
>   const input: GetStringInput
>   const output: Result<GetStringOutput, Error>
>   ghost constructor(input: GetStringInput, output: Result<GetStringOutput, Error>) 
>     ensures this.input == input
>     ensures this.output == output
>   {
>     this.input := input;
>     this.output := output;
>   }
>   static predicate WasNthLastWith(history: History, n: nat, p: GetStringEvent -> bool) 
>     reads history
>   {
>     && n < |history.events| 
>     && var e: Event := history.events[|history.events| - 1 - n];
>     && e is GetStringEvent
>     && var e' := e as GetStringEvent;
>     && p(e')
>   }
> 
30,32c48,66
<  ghost var GetString: seq<DafnyCallEvent<GetStringInput, Result<GetStringOutput, Error>>>
<  ghost var GetStringSingleValue: seq<DafnyCallEvent<GetStringInput, Result<GetStringOutput, Error>>>
<  ghost var GetStringUTF8: seq<DafnyCallEvent<GetStringInput, Result<GetStringOutput, Error>>>
---
> class GetStringSingleValueEvent extends Event {
>   const input: GetStringInput
>   const output: Result<GetStringOutput, Error>
>   ghost constructor(input: GetStringInput, output: Result<GetStringOutput, Error>) 
>     ensures this.input == input
>     ensures this.output == output
>   {
>     this.input := input;
>     this.output := output;
>   }
>   static predicate WasNthLastWith(history: History, n: nat, p: GetStringSingleValueEvent -> bool) 
>     reads history
>   {
>     && n < |history.events| 
>     && var e: Event := history.events[|history.events| - 1 - n];
>     && e is GetStringSingleValueEvent
>     && var e' := e as GetStringSingleValueEvent;
>     && p(e')
>   }
33a68,90
> class GetStringUTF8Event extends Event {
>   const input: GetStringInput
>   const output: Result<GetStringOutput, Error>
>   ghost constructor(input: GetStringInput, output: Result<GetStringOutput, Error>) 
>     ensures this.input == input
>     ensures this.output == output
>   {
>     this.input := input;
>     this.output := output;
>   }
>   static predicate WasNthLastWith(history: History, n: nat, p: GetStringUTF8Event -> bool) 
>     reads history
>   {
>     && n < |history.events| 
>     && var e: Event := history.events[|history.events| - 1 - n];
>     && e is GetStringUTF8Event
>     && var e' := e as GetStringUTF8Event;
>     && p(e')
>   }
> }
> 
> 
> 
59,60d115
<  ensures ValidState() ==> History in Modifies
<   ghost const History: ISimpleTypesStringClientCallHistory
63c118
<  method GetString ( input: GetStringInput )
---
>  method GetString ( input: GetStringInput, ghost history: History? := null )
67,68c122,123
<  modifies Modifies - {History} ,
<  History`GetString
---
>  requires history !in Modifies
>  modifies Modifies , history
70c125
<  decreases Modifies - {History}
---
>  decreases Modifies
74c129,134
<  ensures History.GetString == old(History.GetString) + [DafnyCallEvent(input, output)]
---
>  ensures history != null ==> history.NewEventSuchThat((e: Event) => 
>   && e is GetStringEvent 
>   && var e' := e as GetStringEvent;
>   && e'.input == input 
>   && e'.output == output)
>  ensures history !in Modifies
78c138
<  method GetStringSingleValue ( input: GetStringInput )
---
>  method GetStringSingleValue ( input: GetStringInput, ghost history: History? := null )
82,83c142,143
<  modifies Modifies - {History} ,
<  History`GetStringSingleValue
---
>  requires history !in Modifies
>  modifies Modifies , history
85c145
<  decreases Modifies - {History}
---
>  decreases Modifies
89c149,154
<  ensures History.GetStringSingleValue == old(History.GetStringSingleValue) + [DafnyCallEvent(input, output)]
---
>  ensures history != null ==> history.NewEventSuchThat((e: Event) => 
>   && e is GetStringSingleValueEvent 
>   && var e' := e as GetStringSingleValueEvent;
>   && e'.input == input 
>   && e'.output == output)
>  ensures history !in Modifies
93c158
<  method GetStringUTF8 ( input: GetStringInput )
---
>  method GetStringUTF8 ( input: GetStringInput, ghost history: History? := null )
97,98c162,163
<  modifies Modifies - {History} ,
<  History`GetStringUTF8
---
>  requires history !in Modifies
>  modifies Modifies , history 
100c165
<  decreases Modifies - {History}
---
>  decreases Modifies
104,105c169,175
<  ensures History.GetStringUTF8 == old(History.GetStringUTF8) + [DafnyCallEvent(input, output)]
<  
---
>  ensures history != null ==> history.NewEventSuchThat((e: Event) => 
>   && e is GetStringUTF8Event 
>   && var e' := e as GetStringUTF8Event;
>   && e'.input == input 
>   && e'.output == output)
>  ensures history !in Modifies
> 
144a215
>  import opened Histories
153d223
<  && fresh(res.value.History)
162d231
<  && fresh(History)
168,169c237
<  && History !in Operations.ModifiesInternalConfig(config)
<  && Modifies == Operations.ModifiesInternalConfig(config) + {History}
---
>  && Modifies == Operations.ModifiesInternalConfig(config)
173c241
<  method GetString ( input: GetStringInput )
---
>  method GetString ( input: GetStringInput, ghost history: History? := null )
177,178c245,246
<  modifies Modifies - {History} ,
<  History`GetString
---
>  requires history !in Modifies
>  modifies Modifies , history
180c248
<  decreases Modifies - {History}
---
>  decreases Modifies
184c252,256
<  ensures History.GetString == old(History.GetString) + [DafnyCallEvent(input, output)]
---
>  ensures history != null ==> history.NewEventSuchThat((e: Event) => 
>   && e is GetStringEvent 
>   && var e' := e as GetStringEvent;
>   && e'.input == input 
>   && e'.output == output)
187c259,262
<  History.GetString := History.GetString + [DafnyCallEvent(input, output)];
---
>  if history != null {
>   var event := new GetStringEvent(input, output);
>   history.AddEvent(event);
>  }
193c268
<  method GetStringSingleValue ( input: GetStringInput )
---
>  method GetStringSingleValue ( input: GetStringInput, ghost history: History? := null )
197,198c272,273
<  modifies Modifies - {History} ,
<  History`GetStringSingleValue
---
>  requires history !in Modifies
>  modifies Modifies , history
200c275
<  decreases Modifies - {History}
---
>  decreases Modifies
204c279,283
<  ensures History.GetStringSingleValue == old(History.GetStringSingleValue) + [DafnyCallEvent(input, output)]
---
>  ensures history != null ==> history.NewEventSuchThat((e: Event) => 
>   && e is GetStringSingleValueEvent 
>   && var e' := e as GetStringSingleValueEvent;
>   && e'.input == input 
>   && e'.output == output)
207c286,289
<  History.GetStringSingleValue := History.GetStringSingleValue + [DafnyCallEvent(input, output)];
---
>  if history != null {
>   var event := new GetStringSingleValueEvent(input, output);
>   history.AddEvent(event);
>  }
213c295
<  method GetStringUTF8 ( input: GetStringInput )
---
>  method GetStringUTF8 ( input: GetStringInput, ghost history: History? := null )
217,218c299,300
<  modifies Modifies - {History} ,
<  History`GetStringUTF8
---
>  requires history !in Modifies
>  modifies Modifies , history
220c302
<  decreases Modifies - {History}
---
>  decreases Modifies
224c306,310
<  ensures History.GetStringUTF8 == old(History.GetStringUTF8) + [DafnyCallEvent(input, output)]
---
>  ensures history != null ==> history.NewEventSuchThat((e: Event) => 
>   && e is GetStringUTF8Event 
>   && var e' := e as GetStringUTF8Event;
>   && e'.input == input 
>   && e'.output == output)
227c313,316
<  History.GetStringUTF8 := History.GetStringUTF8 + [DafnyCallEvent(input, output)];
---
>  if history != null {
>   var event := new GetStringUTF8Event(input, output);
>   history.AddEvent(event);
>  }

[lavaleri]

I would like to see the diff in how History is used in method ensures, as that is where we are primarily using them in our code right now. e.g.: https://github.com/aws/aws-cryptographic-material-providers-library-java/blob/main/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy#L154-L159

I understand the tests below sort of approximate this, but it's still hard to grok what the exact scope of changes to our libraries would have to be with this change.

[lavaleri]

Coming back to this, the thing I am having a hard time imagining is where in our clients we would be creating history, and how we would be passing it around. i.e. every time we create a new client, would we also need to create an accompanying history?

[robin-aws]

No we'd be creating a single history object at "the beginning of Dafny execution" and threading it through. I realize that's not very prescriptive in general, but at least in a polymorph library that uses other clients I expect it would make sense to create one at the beginning of each operation (since that's where external code calls into Dafny).

It's possible it would work well for the ***Service module to create the history and pass it into the ***Operations module, but I still have to actually try that.

Thanks for the link, I'll see if I can expand the POC to show the equivalent of that kind of check too.

[lavaleri]

Is this not a ghost?

[robin-aws]

It's automatically inferred to be (since the History constructor is ghost if nothing else), so not necessary to explicitly add the ghost keyword, but I will just to be clearer.

[robin-aws]

Closing this as I'm re-evaluating the design somewhat.