bf2c71d

Propose an implementation of deque

jeehoonkang Aug 30, 2017

f004b7c

Rewording

jeehoonkang Oct 11, 2017

42e6972

Revise

jeehoonkang Dec 27, 2017

f8e624a

Restart the proof

jeehoonkang Dec 29, 2017

da2c665

Prove (VIEW)

jeehoonkang Dec 29, 2017

9f6300c

Prove (SEQ) for owner methods

jeehoonkang Jan 1, 2018

bd7362d

Fix bugs

jeehoonkang Jan 1, 2018

10badde

Prove (SEQ) for successful steal()

jeehoonkang Jan 1, 2018

a25acfe

Prove (SEQ)

jeehoonkang Jan 1, 2018

f9eebcf

Cleanup

jeehoonkang Jan 1, 2018

1c3bab6

Cleanup

jeehoonkang Jan 1, 2018

8f9eb43

Remove synchronization of L204

jeehoonkang Jan 3, 2018

411aa35

WIP

jeehoonkang Jan 4, 2018

d4c6e87

Fix bug and lower orderings

jeehoonkang Jan 5, 2018

0f6aca6

Finish refactoring

jeehoonkang Jan 5, 2018

f40815a

Add discussion

jeehoonkang Jan 7, 2018

06da131

Change date and name

jeehoonkang Jan 7, 2018

7f54b7d

Add discussion on the strange C11 requirement

jeehoonkang Jan 7, 2018

68ffb44

Prove deque returns the right values

jeehoonkang Jan 8, 2018

36884aa

Revise

jeehoonkang Jan 9, 2018

b104076

Change linearization order and reduce promising reasoning

jeehoonkang Jan 9, 2018

2ebbd4b

Change the opinion on data races

jeehoonkang Jan 11, 2018

c8ef1f5

Revise

jeehoonkang Jan 11, 2018

232604c

Revise

jeehoonkang Jan 13, 2018

58b94a9

Discuss the acquire fence in pop()'s race case

jeehoonkang Jan 13, 2018

635e2d8

Wording

jeehoonkang Jan 15, 2018

ac05981

Rewording the proof of (VIEW)

jeehoonkang Jan 15, 2018

ac7d9c1

Rewording the proof of (SEQ)

jeehoonkang Jan 15, 2018

c2e1fb7

Apply @stjepang's comments

jeehoonkang Jan 18, 2018

ec1e35d

Discuss an ARM implementation

jeehoonkang Jan 19, 2018

bcc1db6

Use Retry

jeehoonkang Mar 2, 2018

afaafb5

Fix bug

jeehoonkang Mar 3, 2018

96324bc

Revise the proof according to @hans89's comments

jeehoonkang Mar 22, 2018

a41b50b

Revise the discussion on data races

jeehoonkang Apr 7, 2018