Safe CHANGE-CLASS on SICL objects with no double-word CAS

sicl_rack_update.tla

-------------------------- MODULE sicl_rack_update --------------------------
EXTENDS Naturals, TLC

(* --algorithm basic
variables object = <<0, 0>>;

process ChangeClass \in 1..4
variables oldclass = 0, oldrack = 0;
begin
LoadClass:
  oldclass := object[1];
LoadObject:
  oldrack := object[2];
  (* Wait for a consistent view. We can't to "help"
     and put in a new rack, so it is necessary to wait :( *)
  if oldclass /= oldrack then
    goto LoadClass;
  end if;
  (* So now we have a consistent copy. *)
TryToUpdateClass:
  if object[1] = oldclass then
    object[1] := self;
  else
    goto LoadClass;
  end if;
TryToUpdateRack:
  if object[2] = oldrack then
    object[2] := self;
  else
    goto LoadClass;
  end if;
end process

end algorithm *)

ConsistentAtEnd == \E self \in ProcSet: pc[self] /= "Done" \/ object[1] = object[2]