Fix the documentation according to the memory modelmemory_model_dev

Also, change the ordering requirements of some operations.

4 files changed, 36 insertions, 38 deletions

diff --git a/arch/x86/machine/cpu.h b/arch/x86/machine/cpu.h
index dcb1801..67111d2 100644
--- a/arch/x86/machine/cpu.h
+++ b/arch/x86/machine/cpu.h
@@ -266,7 +266,7 @@ cpu_get_ ## name(void)                                                      \
 {                                                                           \
     unsigned long name;                                                     \
                                                                             \
-    asm volatile("mov %%" __QUOTE(name) ", %0" : "=r" (name) : : "memory"); \
+    asm volatile("mov %%" __QUOTE(name) ", %0" : "=r" (name));              \
     return name;                                                            \
 }                                                                           \
                                                                             \
@@ -285,7 +285,7 @@ cpu_set_ ## name(unsigned long value)                                       \
  *
  * Setting a control register executes a serializing instruction.
  *
- * These are intra-thread release-acquire operations.
+ * There is a strong sequence point when setting a control register.
  */
 CPU_DECL_GETSET_CR(cr0)
 CPU_DECL_GETSET_CR(cr2)
@@ -295,7 +295,7 @@ CPU_DECL_GETSET_CR(cr4)
 /*
  * Enable local interrupts.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_intr_enable(void)
@@ -306,7 +306,7 @@ cpu_intr_enable(void)
 /*
  * Disable local interrupts.
  *
- * This is an intra-thread acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_intr_disable(void)
@@ -317,7 +317,7 @@ cpu_intr_disable(void)
 /*
  * Restore the content of the EFLAGS register, possibly enabling interrupts.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_intr_restore(unsigned long flags)
@@ -332,7 +332,7 @@ cpu_intr_restore(unsigned long flags)
  * Disable local interrupts, returning the previous content of the EFLAGS
  * register.
  *
- * This is an intra-thread acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_intr_save(unsigned long *flags)
@@ -356,7 +356,7 @@ cpu_intr_enabled(void)
 /*
  * Spin-wait loop hint.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_pause(void)
@@ -371,7 +371,7 @@ cpu_pause(void)
  * allow the processor handling them before entering the idle state if they
  * were disabled before calling this function.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_idle(void)
@@ -382,7 +382,7 @@ cpu_idle(void)
 /*
  * Halt the CPU.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 noreturn static __always_inline void
 cpu_halt(void)
@@ -472,7 +472,7 @@ cpu_has_feature(const struct cpu *cpu, enum cpu_feature feature)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_enable_pse(void)
@@ -485,7 +485,7 @@ cpu_enable_pse(void)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_enable_pae(void)
@@ -507,7 +507,7 @@ cpu_has_global_pages(void)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_enable_global_pages(void)
@@ -520,7 +520,7 @@ cpu_enable_global_pages(void)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_cpuid(unsigned int *eax, unsigned int *ebx, unsigned int *ecx,
@@ -550,7 +550,7 @@ cpu_get_msr64(uint32_t msr)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 cpu_set_msr(uint32_t msr, uint32_t high, uint32_t low)
@@ -563,7 +563,7 @@ cpu_set_msr(uint32_t msr, uint32_t high, uint32_t low)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 cpu_set_msr64(uint32_t msr, uint64_t value)
@@ -580,7 +580,7 @@ cpu_set_msr64(uint32_t msr, uint64_t value)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_tlb_flush(void)
@@ -593,7 +593,7 @@ cpu_tlb_flush(void)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_tlb_flush_all(void)
@@ -621,7 +621,7 @@ cpu_tlb_flush_all(void)
  *
  * This function executes a serializing instruction.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static __always_inline void
 cpu_tlb_flush_va(unsigned long va)
@@ -661,8 +661,9 @@ uint64_t cpu_get_freq(void);
 /*
  * Busy-wait for a given amount of time, in microseconds.
  *
- * If the function produces a delay, i.e. the duration argument is strictly
- * greater than zero, this is an intra-thread release-acquire operation.
+ * If calling this function produces a delay, i.e. the duration argument
+ * is strictly greater than zero, there is a strong sequence point during
+ * this operation.
  */
 void cpu_delay(unsigned long usecs);
 
diff --git a/kern/atomic.h b/kern/atomic.h
index 2ecb28f..04a08f3 100644
--- a/kern/atomic.h
+++ b/kern/atomic.h
@@ -24,9 +24,6 @@
  * Some configurations may not support 64-bit operations. Check if the
  * ATOMIC_HAVE_64B_OPS macro is defined to find out.
  *
- * TODO Replace mentions of "memory barriers" throughout the code with
- * C11 memory model terminology.
- *
  * TODO Decide if architecture-specific atomic operations should be
  * provided, and if so, how.
  */
diff --git a/kern/rcu.h b/kern/rcu.h
index eb82a6a..5566331 100644
--- a/kern/rcu.h
+++ b/kern/rcu.h
@@ -80,24 +80,24 @@ struct rcu_reader;
 /*
  * Enter a read-side critical section.
  *
- * This is an intra-thread acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 rcu_read_enter(void)
 {
     rcu_reader_inc(thread_rcu_reader(thread_self()));
-    latomic_fence(LATOMIC_ACQ_REL);
+    latomic_fence(LATOMIC_SEQ_CST);
 }
 
 /*
  * Leave a read-side critical section.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 rcu_read_leave(void)
 {
-    latomic_fence(LATOMIC_ACQ_REL);
+    latomic_fence(LATOMIC_SEQ_CST);
     rcu_reader_dec(thread_rcu_reader(thread_self()));
 }
 
diff --git a/kern/thread.h b/kern/thread.h
index 75ff4b2..9afad46 100644
--- a/kern/thread.h
+++ b/kern/thread.h
@@ -229,7 +229,7 @@ void thread_join(struct thread *thread);
  * the thread is awoken.
  *
  * If this function causes the current thread to yield the processor,
- * this is an intra-thread release-acquire operation.
+ * there is a strong sequence point during this operation.
  */
 void thread_sleep(struct spinlock *interlock, const void *wchan_addr,
                   const char *wchan_desc);
@@ -272,7 +272,7 @@ int thread_resume(struct thread *thread);
  * Suspend execution of the calling thread.
  *
  * If this function causes the calling thread to yield the processor,
- * this is an intra-thread release-acquire operation.
+ * there is a strong sequence point during this operation.
  */
 void thread_delay(uint64_t ticks, bool absolute);
 
@@ -545,7 +545,7 @@ thread_pinned(void)
 /*
  * Pin the current thread to the current processor.
  *
- * This is an intra-thread release-acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_pin(void)
@@ -561,7 +561,7 @@ thread_pin(void)
 /*
  * Unpin the current thread from the current processor.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_unpin(void)
@@ -592,7 +592,7 @@ thread_preempt_enabled(void)
 /*
  * Disable preemption.
  *
- * This is an intra-thread acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_preempt_disable(void)
@@ -613,7 +613,7 @@ thread_preempt_disable(void)
  * never performs voluntary preemption. This may break real-time behavior
  * and should never be used in application code.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_preempt_enable_no_resched(void)
@@ -635,7 +635,7 @@ thread_preempt_enable_no_resched(void)
 /*
  * Enable preemption.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_preempt_enable(void)
@@ -653,7 +653,7 @@ thread_preempt_enable(void)
 /*
  * Disable preemption and interrupts.
  *
- * This is an intra-thread acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_preempt_disable_intr_save(unsigned long *flags)
@@ -665,7 +665,7 @@ thread_preempt_disable_intr_save(unsigned long *flags)
 /*
  * Enable preemption and restore interrupts.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_preempt_enable_intr_restore(unsigned long flags)
@@ -705,7 +705,7 @@ thread_check_intr_context(void)
 /*
  * Enter interrupt context.
  *
- * This is an intra-thread acquire operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_intr_enter(void)
@@ -726,7 +726,7 @@ thread_intr_enter(void)
 /*
  * Leave interrupt context.
  *
- * This is an intra-thread release operation.
+ * There is a strong sequence point during this operation.
  */
 static inline void
 thread_intr_leave(void)