summaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* SI-9302 -Xdisable-assertions raises elide levelSom Snytt2015-05-053-7/+6
| | | | | | | | | | Previously, the flag caused any elidable to be elided. This commit simply sets -Xelide-below to ASSERTION + 1. The flag is useful because there's no mnemonic for specifying the magic constant as an option argument. `-Xelide-below ASSERTION` means asserts are enabled.
* SI-9298 Fix erasure of value classes in JavaJason Zaugg2015-05-051-0/+2
| | | | | | | | | | | | Value classes that appear in signatures of Java defined methods should not be erased to the underlying type. Before this change, we'd get a `ClassCastException`, as the Scala call site would unbox the value class despite the fact the Java recipient would expect the boxed representation. I've tested this for primitive and object wrapped types in parameter and return position.
* Merge pull request #4475 from smarter/fix/old-spec-linksLukas Rytz2015-05-042-2/+2
|\ | | | | Remove references to the old PDF version of the specification
| * Remove references to the old PDF version of the specificationGuillaume Martres2015-04-302-2/+2
| |
* | Merge pull request #4486 from mpociecha/ticket/8679Lukas Rytz2015-05-044-5/+20
|\ \ | | | | | | SI-8679 Add support for ScalaLongSignature attribute in scalap
| * | SI-8679 Add support for ScalaLongSignature attribute in scalapMichał Pociecha2015-05-034-5/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | scalap didn't support really big class files. It was returning an empty String for such files. The reason was that there were only ScalaSignatures taken into account. This commit adds support for ScalaLongSignature. We try to get such an attribute when we didn't find ScalaSignature. Also there's added an additional case to the logic retrieving bytes for a signature. Since ScalaLongSignature can contain many parts, we have to merge their byte arrays. Changes are tested by a new partest-based test. These two files are really big, but it was required (t8679.scala is a reduced version of BigScalaClass - an example attached to JIRA). There are also added TODOs with a JIRA ticket: We have three places, where we process Scala signatures. In the future it would be better to reuse some common logic, if it's possible.
* | | Merge pull request #4467 from nafg/patch-1Lukas Rytz2015-05-041-2/+2
|\ \ \ | | | | | | | | Fix scaladoc of Try#failed
| * | | Fix scaladoc of Try#failednafg2015-04-241-2/+2
| | | | | | | | | | | | | | | | | | | | The documentation stated that it returns a Success[Throwable] regardless, either containing the failure or an UnsupportedOperationException. However only Failure#failed returns a success; Success#failed returns a Failure. Also the phrasing of "Completes this `Try`" and "that `Try` failed with" sounds like it was copy-pasted from Future? Trys don't complete, nor fail, they are immutable.
* | | | Merge pull request #4463 from retronym/topic/indylambda-emit-indyLukas Rytz2015-05-047-23/+147
|\ \ \ \ | | | | | | | | | | Use LambdaMetafactory where possible for lambda creation.
| * | | | Small refactorings and additional comments in DelambdafyJason Zaugg2015-04-221-46/+54
| | | | |
| * | | | Update internal documentation in Delambdafy phaseJason Zaugg2015-04-221-5/+12
| | | | |
| * | | | Support specialized method-handle based lambdasJason Zaugg2015-04-213-7/+27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ``` scala> (x: Int) => {??? : Int} res2: Int => Int = $$Lambda$1371/1961176822@6ed3ccb2 scala> res2(42) scala.NotImplementedError: an implementation is missing at scala.Predef$.$qmark$qmark$qmark(Predef.scala:225) at .$anonfun$1(<console>:8) at $$Lambda$1371/1961176822.apply$mcII$sp(Unknown Source) ... 33 elided scala> (x: Int, y: Long) => {??? : Int} res4: (Int, Long) => Int = $$Lambda$1382/1796047085@6f8e8894 scala> res4(0, 0L) scala.NotImplementedError: an implementation is missing at scala.Predef$.$qmark$qmark$qmark(Predef.scala:225) at .$anonfun$1(<console>:8) at $$Lambda$1382/1796047085.apply$mcIIJ$sp(Unknown Source) ... 33 elided ```
| * | | | SI-8359 Emit invokedynamic for lambdasJason Zaugg2015-04-215-12/+101
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Suitable lambdas are identified in Delambdafy and marked with such with a tree annotation that includes the data needed by the backend to emit an invokedynamic instruction. GenBCode to rewrite instantiation of such anonymous function classes with an invokedynamic instruction. At this stage, I don't plan to merge the support for this into GenASM. Between these points, the lambda capture is represented as an application of a dummy factory symbol: ``` <dummy>(captures...) : FunctionN ``` Demo: ``` % wget http://central.maven.org/maven2/org/scala-lang/modules/scala-java8-compat_2.11/0.3.0/scala-java8-compat_2.11-0.3.0.jar % qscala -classpath scala-java8-compat_2.11-0.3.0.jar -Ydelambdafy:method -target:jvm-1.8 -Ybackend:GenBCode Welcome to Scala version 2.11.6-20150309-144147-c91c978c81 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_25). Type in expressions to have them evaluated. Type :help for more information. scala> (() => "").getClass res0: Class[_ <: () => String] = class $$Lambda$1/871790326 ``` I have also corrected an error in a previous commit. The newly added symbol test, `isDelambdafyTarget`, needs to check for the `ARTIFACT` flag, as that is what is added to the method by `Uncurry`.
* | | | | Merge pull request #4470 from swaldman/correct-predef-assertion-docLukas Rytz2015-05-041-2/+2
|\ \ \ \ \ | | | | | | | | | | | | Fix documentation of assertions in Predef
| * | | | | Fixed documentation of assertions in Predefswaldman2015-04-281-2/+2
| | |_|/ / | |/| | | | | | | | Assertions can be elided at compile time; they generate no runtime conditional code and are in fact run unconditionally if not elided during compilation. Updated documentation to reflect that.
* | | | | Merge pull request #4469 from retronym/ticket/9282Lukas Rytz2015-05-041-3/+5
|\ \ \ \ \ | | | | | | | | | | | | SI-9282 Avoid obscuring an exception during classfile parsing
| * | | | | SI-9282 Avoid obscuring an exception during classfile parsingJason Zaugg2015-04-271-3/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Based on analysis of a stack trace in this bug report, I identified a code path in `ClassfileParser` that can lead to an NPE in its exception handling code. If `val in = new AbstractFileReader(file)` throws (e.g during its construction in which it eagerly reads the file `val buf: Array[Byte] = file.toByteArray`), the call to `in.file` in `handleError` will NPE. This commit stores the active file directly a field in ClassfileParser and uses this in the error reporting.
* | | | | | Merge pull request #4473 from retronym/ticket/9285Lukas Rytz2015-05-041-1/+1
|\ \ \ \ \ \ | | | | | | | | | | | | | | SI-9285 Don't warn about non-sensible equals in synthetic methods
| * | | | | | SI-9285 Don't warn about non-sensible equals in synthetic methodsJason Zaugg2015-04-291-1/+1
| | |/ / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Notably, in the synthetic equals method of a case class. Otherwise, we get an unsuppressable warning when defining a case class with a `Unit`-typed parameter, which some folks use a placeholder for real type while evolving a design.
* | | | | | Merge pull request #4487 from mpociecha/remove-unused-source-classLukas Rytz2015-05-041-127/+0
|\ \ \ \ \ \ | | | | | | | | | | | | | | Remove unused, mostly commented out doc/html/page/Source.scala
| * | | | | | Remove unused, mostly commented out doc/html/page/Source.scalaMichał Pociecha2015-05-021-127/+0
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This file seems to be some early, unfinished draft. It's unused and mostly commented out. De facto it hasn't been changed since this version: https://github.com/scala/scala/blob/d9e3dde6d6d18b9a93e7566447cc3ee342f033d5/src/compiler/scala/tools/nsc/doc/html/page/Source.scala Just in meantime someone updated imports, moved it to other package etc. but nothing more.
* | | | | | Merge pull request #4488 from gbasler/topic/files-in-wrong-placeLukas Rytz2015-05-045-76/+1
|\ \ \ \ \ \ | | | | | | | | | | | | | | Cleanup files in wrong place
| * | | | | | Avoid `Set` instantiation.Gerard Basler2015-05-031-2/+1
| | | | | | |
| * | | | | | Move test files to the right place.Gerard Basler2015-05-034-74/+0
| |/ / / / /
* / / / / / Update intellij project files for IDEA 14.1 and latest Scala pluginLukas Rytz2015-05-0142-1054/+175
|/ / / / / | | | | | | | | | | | | | | | | | | | | Removes the src/intellij-14 folder and moves everything back to src/intellij.
* | | | | Merge pull request #4465 from retronym/ticket/9279Lukas Rytz2015-04-271-5/+5
|\ \ \ \ \ | |_|_|/ / |/| | | | SI-9279 Improve performance of bash runner script
| * | | | SI-9279 Improve performance of bash runner scriptJason Zaugg2015-04-231-5/+5
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In fbe897d16, the template for bash scripts (scala/scalac/etc) was modified to fix processing of `-J`, `-bootcp`. This involved looping through the argument array and filtering out options like `-bootcp` that only influence the script, and shouldn't be passed to the JVM. However, the mechanism to do this uses an inefficient, erm, "CanBuildFrom", and under the load of even a few hundred source files takes half a second before the JVM starts. Throw 2000 files at it, and you have to wait ten seconds! This commit uses a more efficient array append operator. This requires Bash 3 or above. Hopefully it is safe to presume this version these days, it's been around for a decade. Results: ``` % time ~/scala/2.11.6/bin/scalac -J-NOJVM abcdedfghijklmnopqrtsuvwxyv{1..2000} 2>&1 Unrecognized option: -NOJVM Error: Could not create the Java Virtual Machine. Error: A fatal exception has occurred. Program will exit. real 0m7.765s user 0m7.734s sys 0m0.028s % time ./build/quick/bin/scalac -J-NOJVM abcdedfghijklmnopqrtsuvwxyv{1..2000} 2>&1 Unrecognized option: -NOJVM Error: Could not create the Java Virtual Machine. Error: A fatal exception has occurred. Program will exit. real 0m0.144s user 0m0.124s sys 0m0.022s ``` Thanks to Stephan Schmidt for pointing out the performance gulf.
* | | | Merge pull request #4415 from Ichoran/issue/9254Adriaan Moors2015-04-221-5/+7
|\ \ \ \ | | | | | | | | | | SI-9254 UnrolledBuffer appends in wrong position
| * | | | SI-9254 UnrolledBuffer appends in wrong positionRex Kerr2015-03-311-5/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixed two bugs in insertion (insertAll of Unrolled): 1. Incorrect recursion leading to an inability to insert past the first chunk 2. Incorect repositioning of `lastptr` leading to strange `append` behavior after early insertion Added tests checking that both of these things now work. Also added a comment that "waterlineDelim" is misnamed. But we can't fix it now--it's part of the public API. (Shouldn't be, but it is.)
* | | | | Merge pull request #4416 from Ichoran/issue/9197Adriaan Moors2015-04-221-1/+4
|\ \ \ \ \ | | | | | | | | | | | | SI-9197 Duration.Inf not a singleton when deserialized
| * | | | | SI-9197 Duration.Inf not a singleton when deserializedRex Kerr2015-03-311-1/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Made `Duration.Undefined`, `.Inf`, and `.MinusInf` all give back the singleton instance instead of creating a new copy by overriding readResolve. This override can be (and is) private, which at least on Sun's JDK8 doesn't mess with the auto-generated SerialVersionUIDs. Thus, the patch should make things strictly better: if you're on 2.11.7+ on JVMs which pick the same SerialVersionUIDs, you can recover singletons. Everywhere else you were already in trouble anyway.
* | | | | | Merge pull request #4462 from som-snytt/issue/badtabAdriaan Moors2015-04-221-5/+10
|\ \ \ \ \ \ | | | | | | | | | | | | | | SI-9275 Fix row-first display in REPL
| * | | | | | SI-9275 Fix row-first display in REPLSom Snytt2015-04-211-5/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A missing range check in case anyone ever wants to use ``` -Dscala.repl.format=across ``` which was observed only because of competition from Ammonite.
* | | | | | | Merge pull request #4461 from adriaanm/rebase-4446Adriaan Moors2015-04-2245-58/+58
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | Fix many typos
| * | | | | | | Fix many typosMichał Pociecha2015-04-2145-58/+58
| |/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit corrects many typos found in scaladocs and comments. There's also fixed the name of a private method in ICodeCheckers.
* | | | | | | Merge pull request #4452 from lrytz/valueClassSelfTypeBCodeAdriaan Moors2015-04-221-2/+4
|\ \ \ \ \ \ \ | |_|_|_|/ / / |/| | | | | | Don't crash GenBCode for value classes with a self declaration
| * | | | | | Don't crash GenBCode for value classes with a self declarationLukas Rytz2015-04-161-2/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | If a value class has a self declaration class V(x: Long) extends AnyVal { self => /* ... */ } `vClassSymbol.typeOfThis.typeSymbol` is `class Long` in the backend. The InlineInfo for traits contains a field for the self type of the trait. This is required for re-writing calls to final trait methods to the static implementation method: the self type appears in the impl method signature. By mistake, the backend was recording the self type of all classes, not only of traits. In the case of a value class with a self declaration, this broke the assumption that the self type is always a class type (not a primitive type). The simple fix: only record the self type for traits.
* | | | | | | Merge pull request #4464 from gourlaysama/wip/scaladoc-deprecatedVlad Ureche2015-04-225-3/+74
|\ \ \ \ \ \ \ | |_|/ / / / / |/| | | | | | SI-4476 add an index of deprecated members to scaladoc
| * | | | | | SI-4476 add an index of deprecated members to scaladocAntoine Gourlay2015-04-225-3/+74
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The deprecated list is only emitted if there actually are deprecated members; same for the link in the left sidebar. We just build on the existing index support, with an additional method to avoid having to go through the whole index if we won't generate the page anyway. The deprecated list page itself is completely identical to the normal index pages, except we don't strike through any entry (there are *all* deprecated already). There is just about enough space in the left sidebar for the deprecated link, see [1], and [2] for when there are no deprecated members. [1]: http://static.gourlaysama.net/img/scaladoc-deprecated.png [2]: http://static.gourlaysama.net/img/scaladoc-deprecated-empty.png
* | | | | | Merge pull request #4457 from retronym/ticket/9268Adriaan Moors2015-04-211-7/+3
|\ \ \ \ \ \ | | | | | | | | | | | | | | SI-9268 Be robust against absent classfiles during signature parsing
| * | | | | | SI-9268 Be robust against absent classfiles during signature parsingJason Zaugg2015-04-211-7/+3
| | |_|_|/ / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When parsing a Java generic signature that references an inner class `A$B`, we were tripping an assertion if the enclosing class `A` was absent. This commit creates a stub symbol for `B` when this happens, rather than continuing on with `NoSymbol`. The enclosed test shows that we can instantiate a class containing a method referring to such an inner class with only a warning about the absent classfile, and that an error is issued only upon a subsequent attempt to call the method.
* | | | | | Merge pull request #4445 from jedesah/patch-2Adriaan Moors2015-04-211-1/+1
|\ \ \ \ \ \ | |/ / / / / |/| | | | | Fix typo in Quasiquote doc that was confusing
| * | | | | Fix typo in Quasiquote doc that was confusingJean-Rémi Desjardins2015-04-101-1/+1
| | | | | |
* | | | | | Make lambda body public rather than using static accessorJason Zaugg2015-04-172-101/+48
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Under -Ydelambdafy:method (the basis of the upcoming "indylambda" translation for -target:jvm-1.8), an anonymous function is currently encoded as: 1. a private method containing the lambda's code 2. a public, static accessor method that allows access to 1 from other classes, namely: 3. an anonymous class capturing free variables and implementing the suitable FunctionN interface. In our prototypes of indylambda, we do away with 3, instead deferring creating of this class to JDK8's LambdaMetafactory by way of an invokedynamic instruction at the point of lambda capture. This facility can use a private method as the lambda target; access is mediated by the runtime-provided instance of `java.lang.invoke.MethodHandles.Lookup` that confers the privelages of the lambda capture call site to the generated implementation class. Indeed, The java compiler uses this to emit private lambda body methods. However, there are two Scala specific factors that make this a little troublesome. First, Scala's optimizer may want to inline the lambda capture call site into a new enclosing class. In general, this isn't a safe optimization, as `invokedynamic` instructions have call-site specific semantics. But we will rely the ability to inline like this in order to eliminate closures altogether where possible. Second, to support lambda deserialization, the Java compiler creates a synthetic method `$dersializeLamda$` in each class that captures them, just to be able to get the suitable access to spin up an anoymous class with access to the private method. It only needs to do this for functional interfaces that extends Serializable, which is the exception rather than the rule. But in Scala, *every* function must support serialization, so blindly copying the Java approach will lead to some code bloat. I have prototyped a hybrid approach to these challenges: use the private method directly where it is allowed, but fall back to using the accessor method in a generic lambda deserializer or in call sites that have been inlined into a new enclosing class. However, the most straight forward approach is to simply emit the lambda bodies as public (with an mangled name and with the SYHTNETIC flag) and use them in all cases. That is what is done in this commit. This does moves us one step backwards from the goals of SI-7085, but it doesn't seem sensible to incur the inconvenience from locking down one small part of our house when we don't have a plan or the budget to complete that job. The REPL has some fancy logic to decompile the bodys of lambdas (`:javap -fun C#m`) which needed tweaking to accomodate this change. I haven't tried to make this backwards compatible with the old encoding as `-Ydelambdafy:method` is still experimental.
* | | | | | Merge pull request #4451 from som-snytt/issue/3368-remediateAdriaan Moors2015-04-162-5/+4
|\ \ \ \ \ \ | |_|/ / / / |/| | | | | SI-3368 Default to coalescing for 2.11
| * | | | | SI-3368 Default to coalescing for 2.11Som Snytt2015-04-162-5/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Preserve current behavior (no PCData nodes, only Text) for 2.11. The coalescing flag is on if enabled or if source level is not 2.12 and no flag was supplied. The subtle change is that adjacent Text nodes are thereby coalesced. This happens in the presence of CData sections, but this is at the discretion of the parser anyway. Also, no PCData nodes are emitted under coalescing, even if there were no sibling text nodes. That is the correct behavior: the general idea is that coalescing mode says, I only want to deal with text.
* | | | | | SI-9273 Avoid unpositioned error for bare classOfJason Zaugg2015-04-151-4/+5
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A bare identifier `classOf` in a position wth an expected type of `Class[_]` was leading to an unpositioned error. This is due to special treatment of bare `classOf` in `typedIdent` creating an ephemeral, but unpositioned, `TypeTree`. This commit positions that tree and tests that the error is issued at a sensible position. There is still an irregularity between `classOf` and `Predef.classOf`, but that seems esoteric enough to leave alone for now.
* | | | | | Merge pull request #4367 from retronym/topic/indylambda-specializationAdriaan Moors2015-04-131-1/+17
|\ \ \ \ \ \ | |/ / / / / |/| | | | | Disable -Ydelambdafy:method for specialized FunctionN
| * | | | | Disable -Ydelambdafy:method for specialized FunctionNJason Zaugg2015-04-101-1/+17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The Delambdafy phase generates its `FunctionN` subclasses after the specialization phase. As such, `((x: Int) => x).apply(42)` incurs boxing. This commit falls back to the `-Ydelambdafy:inline` in this case. This is done by running the specialization type map over the type of the function, and seeing if anything changes. To make this work robustly, we first need to ensure that the specialization info transformer has processed all the function types. This is not a fundamental limitation; we could in principle generate the specialized code. A followup change will use `-Ydelambdafy:method` as the basis for invokedymnamic lambdas. As part of that stream of work, we will synthesize specialization-aware lambdas, and remove the fallback to `-Ydelambdafy:inline`. I have updated some tests that intend to test the delambdafy transform to avoid use of specialized function types.
* | | | | | Merge pull request #4431 from adriaanm/rebase-4379Adriaan Moors2015-04-133-41/+165
|\ \ \ \ \ \ | |_|/ / / / |/| | | | | Patmat: efficient reasoning about mutual exclusion