Consider this example:

// thread A:
start_transaction();
update_mysql();
commit_transaction();
remove_redis_cache("key");

// thread B:
std::string msg;
bool r = read_redis_cache("key",msg);
if(r){
 return msg;
}
const std::string msg = read_mysql();
update_redis_cache("key",msg);

Assuming there exists cached data in Redis before threads A and B run. So, in this program, can thread B read the old data from MySQL and update the Redis cache with it?

The issue is that thread B cannot read the cached data from Redis only if thread A removes the cached data, and the operation occurs after the transaction has been committed. From implementations, these operations are all external IO operations whose side effects are unknown to implementations; the implementations would be very conservative to reorder these operations.

Instead, from the abstract machine sense, we just need to do formal reasoning. So, I wonder, can we simply view these external IO (multithreaded safe)operations as seq_cst operations to do multithreaded observable behavior reasoning in terms of a single total order?