I use a tag masked into the stored data to try prevent the ABA problem.

Every thread has its own unique tag.

  long original = me->realend;                                                                                                              
  int tag = (original & TAG_MASK);                                                                                                          
  changed = (((original & END_MASK) >> 32)) % me->size;                                                                                   
  long new = (data->thread_tag) | (((changed + 1) % me->size) << 32); 

Then compare and swap as usual. If another thread updates then they shall fail the compare and swap and we have to reloop and try again.

I am still learning TLA+ to write a model.