X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=README.md;h=23492ebfc671a0873dd58fe4091e11526adf9161;hp=37eb96265e56d130ea288471c666e23b68b73268;hb=f1be76b0fb0eefe52864448377df62c81fd9a3e1;hpb=402caea290ab08ddb12cb79cbf73ec7e97066863 diff --git a/README.md b/README.md index 37eb962..23492eb 100644 --- a/README.md +++ b/README.md @@ -146,7 +146,7 @@ variable, for instance. Reading an execution trace -------------------------- -When CDSChecker detects a bug in your program (or when run with the --verbose +When CDSChecker detects a bug in your program (or when run with the `--verbose` flag), it prints the output of the program run (STDOUT) along with some summary trace information for the execution in question. The trace is given as a sequence of lines, where each line represents an operation in the execution @@ -166,8 +166,8 @@ The following list describes each of the columns in the execution trace output: * Action type: The type of operation performed - * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where XXX is - relaxed, release, acquire, rel_acq, or seq_cst) + * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is + `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`) * Location: The memory location on which this operation is operating. This is well-defined for atomic write/read/RMW, but other operations are subject to @@ -176,11 +176,11 @@ The following list describes each of the columns in the execution trace output: * Value: For reads/writes/RMW, the value returned by the operation. Note that for RMW, this is the value that is *read*, not the value that was *written*. For other operations, 'value' may have some CDSChecker-internal meaning, or - it may simply be a don't-care (such as 0xdeadbeef). + it may simply be a don't-care (such as `0xdeadbeef`). * Rf: For reads, the sequence number of the operation from which it reads. [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE), - as printed during --verbose execution, reads may not be resolved and so may + as printed during `--verbose` execution, reads may not be resolved and so may have Rf=? or Rf=Px, where x is a promised future value.] * CV: The clock vector, encapsulating the happens-before relation (see our @@ -226,7 +226,7 @@ HASH 4073708854 Now consider, for example, operation 10: This is the 10th operation in the execution order. It is an atomic read-relaxed -operation performed by thread 3 at memory address 0x601068. It reads the value +operation performed by thread 3 at memory address `0x601068`. It reads the value "0", which was written by the 2nd operation in the execution order. Its clock vector consists of the following values: