fix formatting

diff --git a/personal/_posts/2017-08-11-types-as-contracts-evaluation.md b/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
index 5f0c07a98d1a45d033f938fb2ba6996b9ad641be..08f9bf5faee62677df433d280cf90f6e6ddfaadf 100644 (file)
--- a/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
+++ b/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
@@ -21,7 +21,7 @@ Some of these turned out to be [compiler](https://github.com/rust-lang/rust/issu
 In the following, I describe the patterns that I found.
 I assume that you are familiar with Types as Contracts as introduced in my [previous post]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}).
 
 In the following, I describe the patterns that I found.
 I assume that you are familiar with Types as Contracts as introduced in my [previous post]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}).
 

-## 1.1 Ownership Passing Via Raw Pointers
+### 1.1 Ownership Passing Via Raw Pointers

 
 I already mentioned this in the original post:  `mem::swap` triggers a lock violation in the strictest interpretation of the model.
 {% highlight rust %}
 
 I already mentioned this in the original post:  `mem::swap` triggers a lock violation in the strictest interpretation of the model.
 {% highlight rust %}


@@ -69,12 +69,12 @@ However, this again overlaps with `self`.
 
 This list is not exhaustive by any means; there are problems of this sort pretty much whenever raw pointers are used in non-trivial ways.
 
 
 This list is not exhaustive by any means; there are problems of this sort pretty much whenever raw pointers are used in non-trivial ways.
 

-## 1.2 Uninitialized memory
+### 1.2 Uninitialized memory

 
 Any place that calls `mem::uninitialized` instantly has validation blow up because the returned `T` is, obviously, not actually a valid `T` -- it is, after all, completely uninitialized.
 However, it turns out that `mem::uninitialized` is causing other problems as well (e.g. around uninhabited types), and [better APIs for handling uninitialized data have already been proposed](https://internals.rust-lang.org/t/mem-uninitialized-and-trap-representations/4167/18?u=ralfjung).
 
 
 Any place that calls `mem::uninitialized` instantly has validation blow up because the returned `T` is, obviously, not actually a valid `T` -- it is, after all, completely uninitialized.
 However, it turns out that `mem::uninitialized` is causing other problems as well (e.g. around uninhabited types), and [better APIs for handling uninitialized data have already been proposed](https://internals.rust-lang.org/t/mem-uninitialized-and-trap-representations/4167/18?u=ralfjung).
 

-## 1.3 `Arc::drop`
+### 1.3 `Arc::drop`

 
 This is the most interesting case I found.  The `Arc` destructor ends up calling `Arc::drop_slow`, which is implemented as follows:
 {% highlight rust %}
 
 This is the most interesting case I found.  The `Arc` destructor ends up calling `Arc::drop_slow`, which is implemented as follows:
 {% highlight rust %}


@@ -140,7 +140,7 @@ In particular, it turned out that suspensions were actually not modeling borrowi
 There were also some changes affecting the rules of where validation calls are emitted in some corner cases, but there weren't really any interesting things to learn there.
 At some point I will write down the exact rules in full detail; until then it is really the general approach that matters much more than such corner cases.
 
 There were also some changes affecting the rules of where validation calls are emitted in some corner cases, but there weren't really any interesting things to learn there.
 At some point I will write down the exact rules in full detail; until then it is really the general approach that matters much more than such corner cases.
 

-## 2.1 Suspension of Write Locks
+### 2.1 Suspension of Write Locks

 
 In the original proposal, on every borrow `y = &[mut] x;`, the write locks on `x` would be *suspended*.
 This means that the locks get released, but will be re-acquired (or *recovered*) automatically when the lifetime of the borrow ends.
 
 In the original proposal, on every borrow `y = &[mut] x;`, the write locks on `x` would be *suspended*.
 This means that the locks get released, but will be re-acquired (or *recovered*) automatically when the lifetime of the borrow ends.


@@ -200,7 +200,7 @@ Notice that in the above example, both `x_inner` and `r` have the *same* lifetim
 So, I will have to go back to the drawing board and figure out a different way to identify write locks.
 I have some ideas, but I am not very happy with them.
 
 So, I will have to go back to the drawing board and figure out a different way to identify write locks.
 I have some ideas, but I am not very happy with them.
 

-## 2.2 Unsafe Code
+### 2.2 Unsafe Code

 
 As already indicated in the original post, the way I suggest to handle the problems with raw pointers described in [§1.1](#11-ownership-passing-via-raw-pointers) is by relaxing the validation performed around unsafe code.
 Specifically, the code that emits MIR validation statements now detects if a function is unsafe, contains an unsafe block, or (in the case of closures) is defined inside an unsafe block/function.
 
 As already indicated in the original post, the way I suggest to handle the problems with raw pointers described in [§1.1](#11-ownership-passing-via-raw-pointers) is by relaxing the validation performed around unsafe code.
 Specifically, the code that emits MIR validation statements now detects if a function is unsafe, contains an unsafe block, or (in the case of closures) is defined inside an unsafe block/function.


@@ -219,7 +219,7 @@ In discussions, two possible solutions to this problems became apparent:
 
 Both of these options are certainly worth exploring.
 
 
 Both of these options are certainly worth exploring.
 

-# 3 Testing Your Own Code
+## 3 Testing Your Own Code

 
 The implementation of the model as described above (well, with the open problems mentioned in [§2.1](21-suspension-of-write-locks)) actually landed upstream in rustc and miri, so you can play around with this yourself!
 To do so, you need to install Rust nightly and miri.
 
 The implementation of the model as described above (well, with the open problems mentioned in [§2.1](21-suspension-of-write-locks)) actually landed upstream in rustc and miri, so you can play around with this yourself!
 To do so, you need to install Rust nightly and miri.


@@ -242,7 +242,7 @@ If you find anything odd and things don't work as expected, please [report a bug
 Notice however that miri currently supports virtually no interaction with the surrounding operating system, like file access or spawning threads.
 
 
 Notice however that miri currently supports virtually no interaction with the surrounding operating system, like file access or spawning threads.
 
 

-# 4 Future Work
+## 4 Future Work

 
 As usual, there are so many things that could be done next.
 
 
 As usual, there are so many things that could be done next.