Support running on non-empty database

[serathius]

What would you like to be added?

This task is a little harder as it requires diving into robustness linearization model, interested contributor beware!

Currently we are validating that database is empty before running tests

etcd/tests/antithesis/test-template/robustness/main.go

Lines 96 to 99 in 4976738

	r, err := traffic.CheckEmptyDatabaseAtStart(ctx, lg, hosts, ids, baseTime)
	if err != nil {
	lg.Fatal("Failed empty database at start check", zap.Error(err))
	}

.

This is done by reading revision of etcd before any traffic is sent and checking if revision is equal 1

etcd/tests/robustness/traffic/traffic.go

Lines 207 to 227 in 4976738

	func CheckEmptyDatabaseAtStart(ctx context.Context, lg *zap.Logger, endpoints []string, ids identity.Provider, baseTime time.Time) (report.ClientReport, error) {
	c, err := client.NewRecordingClient(endpoints, ids, baseTime)
	if err != nil {
	return report.ClientReport{}, err
	}
	defer c.Close()
	for {
	rCtx, cancel := context.WithTimeout(ctx, RequestTimeout)
	resp, err := c.Get(rCtx, "key")
	cancel()
	if err != nil {
	lg.Warn("Failed to check if database empty at start, retrying", zap.Error(err))
	continue
	}
	if resp.Header.Revision != 1 {
	return report.ClientReport{}, validate.ErrNotEmptyDatabase
	}
	break
	}
	return c.Report(), nil
	}

. Revision in etcd is a global logical clock for operations that start at 1. This ensures that there were no transactions executed on etcd before so etcd is empty.

This is also checked as first step of validation

etcd/tests/robustness/validate/validate.go

Lines 113 to 127 in 4976738

	func validateEmptyDatabaseAtStart(reports []report.ClientReport) error {
	if len(reports) == 0 {
	return nil
	}
	for _, r := range reports {
	for _, op := range r.KeyValue {
	request := op.Input.(model.EtcdRequest)
	response := op.Output.(model.MaybeEtcdResponse)
	if response.Revision == 1 && request.IsRead() {
	return nil
	}
	}
	}
	return ErrNotEmptyDatabase
	}

. This validation is because this is an implicit assumption of the linearization code, that without this assertion would return hard to discern error.

We can try to improve the linearization to allow non empty code. So why linearization doesn't support non-empty database? Because it needs to a complete view of database, so it can simulate it. Assuming it's empty was just easier to implement.

etcd/tests/robustness/model/deterministic.go

Lines 99 to 108 in 4976738

	func freshEtcdState() EtcdState {
	return EtcdState{
	Revision: 1,
	// Start from CompactRevision equal -1 as etcd allows client to compact revision 0 for some reason.
	CompactRevision: -1,
	KeyValues: map[string]ValueRevision{},
	KeyLeases: map[string]int64{},
	Leases: map[int64]EtcdLease{},
	}
	}

To improve it we could just replace the Read of revision 1 at the beginning with operation to download the state of database and change the model to accept this state as initial one.

Steps;

1. We still need to make a special request at before all other requests. But now instead of checking revision == 1, we just need to read the database state. Changes in

   etcd/tests/antithesis/test-template/robustness/main.go

   Lines 96 to 99 in 4976738

   	r, err := traffic.CheckEmptyDatabaseAtStart(ctx, lg, hosts, ids, baseTime)
   	if err != nil {
   	lg.Fatal("Failed empty database at start check", zap.Error(err))
   	}

   .
2. In validation we still need to confirm if the special Read request is present. However the conditions are different, we need to make sure it precedes all other requests that reads the whole database contents (or at least the prefix of all keys used in the robustness test). Changes in

   etcd/tests/robustness/validate/validate.go

   Lines 113 to 127 in 4976738

   	func validateEmptyDatabaseAtStart(reports []report.ClientReport) error {
   	if len(reports) == 0 {
   	return nil
   	}
   	for _, r := range reports {
   	for _, op := range r.KeyValue {
   	request := op.Input.(model.EtcdRequest)
   	response := op.Output.(model.MaybeEtcdResponse)
   	if response.Revision == 1 && request.IsRead() {
   	return nil
   	}
   	}
   	}
   	return ErrNotEmptyDatabase
   	}

   .
3. We would want to add a way in EtcdState to represent a state that etcd is not initialized, during which the Step method will only allow a read requests. We could hardcode the same request as in step 2.

Why is this needed?

Allow multiple runs of antithesis locally.
/cc @henrybear327 @nwnt

[nwnt]

I can have a look at this.

[serathius]

/assign @nwnt

[serathius]

Would recommend to skip this issue for now, it's pretty complicated and the benefits is limited. I would say it's low priority.

[nwnt]

Roger that. I'm unassigning this from myself for now then.

[nwnt]

/unassign