How to achieve a StoreLoad barrier in C++11?

Options A and B are valid solutions.

• Option A: it doesn't really matter what a seq-cst fence translates to, the C++ standard clearly defines what guarantees it provides. I have laid them out in this post: When is a memory_order_seq_cst fence useful?
• Option B: yes, your reasoning is correct. All modifications on some object have a single total order (the modification order), so you can use that to synchronize the threads and ensure visibility of all side-effects.

However, Option C is not valid! A synchronize-with relation can only be established by acquire/release-operations on the same object. In your case you have two completely different and indepent objects dummy1 and dummy2. But these cannot be used to establish a happens-before relation. In fact, since the atomic variables are purely local (i.e., they are only ever touched by one thread), the compiler is free to remove them based on the as-if rule.

Update

Option A:
I assume set() and check() do operate on some atomic value. Then we have the following situation (-> denotes sequenced-before):

• set()-> fence1(seq_cst) -> y.load()
• y.store(true) -> fence2(seq_cst) -> check()

So we can apply the following rule:

For atomic operations A and B on an atomic object M, where A modifies M and B takes its value, if there are memory_order_seq_cst fences X and Y such that A is sequenced before X, Y is sequenced before B, and X precedes Y in S, then B observes either the effects of A or a later modification of M in its modification order.

I.e., either check() sees that value stored in set, or y.load() sees the value written be y.store() (the operations on y can even use memory_order_relaxed).

Option C:
The C++17 standard states [32.4.3, p1347]:

There shall be a single total order S on all memory_order_seq_cst operations, consistent with the "happens before" order and modification orders for all affected locations [...]

The important word here is "consistent". It implies that if an operation A happens-before an operation B, then A must precede B in S. However, logical implication is a one-way-street, so we cannot infer the inverse: just because some operation C precedes an operation D in S does not imply that C happens before D.

In particular, two seq-cst operations on two separate objects cannot be used to establish a happens before relation, even though the operations are totally ordered in S. If you want to order operations on separate objects, you have to refer to seq-cst-fences (see Option A).