[ fix ] RRBVector1

[Matthew-Mosior]

This PR fixes the RRBVector1 implementation by utilizing casmod1/casupdate1 to ensure thread-safe operations.

Closes #63

[Matthew-Mosior]

@stefan-hoeck This PR fixes the concurrency issue with RRBVector1, I'll probably go ahead and merge soon if I don't hear anything.

[stefan-hoeck]

When looking at the diff, I noticed three things:

• The diff is quite large, larger than just a fix of concurrency issues, so this PR seems to do more than the title claims. Should probably be several PRs for easier reviewing
• You claim to fix concurrency issues, yet you only stress-test one of the supposedly thread-safe functions. How can we be sure that the issue is correctly fixed for the others?
• This is more a general observation: Try to not use assert_total $ idris_crash unless strictly necessary. The array library, for instance, provides several ways for safe indexing into arrays as well as for iterating from the beginning and the end of the array. In my opinion, hacks like assert_total and idris_crash should be used only if proving stuff about your code is otherwise not feasible, as it takes some of the robustness from our code that Idris would otherwise provide.

[Matthew-Mosior]

When looking at the diff, I noticed three things:

* The diff is quite large, larger than just a fix of concurrency issues, so this PR seems to do more than the title claims. Should probably be several PRs for easier reviewing

* You claim to fix concurrency issues, yet you only stress-test one of the supposedly thread-safe functions. How can we be sure that the issue is correctly fixed for the others?

* This is more a general observation: Try to not use `assert_total $ idris_crash` unless strictly necessary. The array library, for instance, provides several ways for safe indexing into arrays as well as for iterating from the beginning and the end of the array. In my opinion, hacks like `assert_total` and `idris_crash` should be used only if proving stuff about your code is otherwise not feasible, as it takes some of the robustness from our code that Idris would otherwise provide.

Good points here:

• This diff is large, however it is necessary as the original design of RRBVector1 was flawed. Previously, it was implemented in a way where there was no easy way to ensure thread-safe operations.
• True, let me add some more stress-tests.
• I agree here, I think this may be better addressed in a follow-up PR.