Replay issues

Problem statement

Replay of deploys with consumes of different types (peek, linear) on the same channel is currently non-deterministic and leads to "unused COMM event" errors in replay.

This is true and easily reproducible for the newly introduced <<- syntax. It looks like the same problem is present in the old registry, but somewhat harder to reproduce (see  RCHAIN-3757 - Getting issue details... STATUS )

Example

Executing the following contract:

p0                                                s0                f0

for(_ <<- @0) { Nil } | @0!(0) | for(_ <- @0) { Nil }


Let's assume that during normal execution (play) the sequence of the events was as follows:

  1. s0 is produced and stored in the tuplespace
  2. p0 is consumed. It matches s0 and produces a COMM event c0. Since s0 was peeked, it isn't removed from the tuplespace
  3. f0 is consumed. It matches s0 and produces a COMM event c1. s0 is removed from the tuplespace


If the execution order during replay is exactly the same it is successful.

If however the following path of execution is chosen the problems manifest themselves:

  1. s0 is produced and stored in the tuplespace
  2.  f0 is consumed. It matches s0 and the event log contains a COMM event c1 (f0, s0) so a COMM event c1 is raised. s0 is removed from the tuplespace
  3. p0 is consumed. s0 is no longer there so the continuation is stored in the tuplespace
  4. Unused COMM event error is raised because c0 never happened

Proposed solution

Description

In order for replay to work correctly ReplayRSpace needs to be able to defer the operation which removes the peeked data from the tuplespace, so that all peeks that produced COMM events can do so again. This would be possible if both sends were distinguishable from one another.

If after being peeked by p0, s0 was removed from the tuplespace and replaced with s1 the execution order would look as follows:

  1. s0 is produced and stored in the tuplespace
  2. p0 is consumed. It matches s0 and produces a COMM event c0 (p0, s0).
  3. s0 was peeked, so p0 triggers a produce of s1
  4. f0 is consumed. It matches s1 and produces a COMM event c1(f0, s1). s1 is removed from the tuplespace

Replay now looks like this:

  1. s0 is produced and stored in the tuplespace
  2. f0 is consumed. It could match s0, but the replay log doesn't contain a COMM event raised by f0 and s0 (f0, s0). f0 is stored in the tuplespace
  3. p0 is consumed. s0 matches. Since the replay log contains a COMM c0(p0, s0), s0 is consumed, the COMM event is raised and s0 is removed from the tuplespace. 
  4. s0 was peeked, so p0 triggers a produce of s1. s1 matches f0 raising a COMM event c1(f0, s1)

Implications

The solution above is going to require changes in RSpace and the Rholang reducer.

In RSpace, the produce operations saved in the replay log will need to contain the counter so that it is available during replay

In the reducer, the peeked data will need to be produced again when a match with a peek continuation happens. This needs to be done in both Reduce.produce and Reduce.consume.