1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995
|
\htmlhr
\chapterAndLabel{Lock Checker}{lock-checker}
The Lock Checker prevents certain concurrency errors by enforcing a
locking discipline. A locking discipline indicates which locks must be held
when a given operation occurs. You express the locking discipline by
declaring a variable's type to have the qualifier
\<\refqualclass{checker/lock/qual}{GuardedBy}{\small("\emph{lockexpr}")}>.
This indicates that the variable's value may
be dereferenced only if the given lock is held.
To run the Lock Checker, supply the
\code{-processor org.checkerframework.checker.lock.LockChecker}
command-line option to javac. The \<-AconcurrentSemantics>
command-line option is always enabled for the Lock Checker (see Section~\ref{faq-concurrency}).
\sectionAndLabel{What the Lock Checker guarantees}{lock-guarantees}
The Lock Checker gives the following guarantee.
Suppose that expression $e$ has type
\<\refqualclass{checker/lock/qual}{GuardedBy}(\ttlcb"x", "y.z"\ttrcb)>.
Then the value computed for $e$ is only dereferenced by a thread when the
thread holds locks \<x> and \<y.z>.
Dereferencing a value is reading or writing one of its fields.
The guarantee about $e$'s value
holds not only if the expression $e$ is dereferenced
directly, but also if the value was first copied into a variable,
returned as the
result of a method call, etc.
Copying a reference is always
permitted by the Lock Checker, regardless of which locks are held.
A lock is held if it has been acquired but not yet released.
Java has two types of locks.
A monitor lock is acquired upon entry to a \<synchronized> method or block,
and is released on exit from that method or block.
% (More precisely,
% the current thread locks the monitor associated with the value of
% \emph{E}; see \href{https://docs.oracle.com/javase/specs/jls/se11/html/jls-17.html#jls-17.1}{JLS \S17.1}.)
An explicit lock is acquired by a method call such as
\sunjavadoc{java.base/java/util/concurrent/locks/Lock.html\#lock()}{Lock.lock()},
and is released by another method call such as
\sunjavadoc{java.base/java/util/concurrent/locks/Lock.html\#unlock()}{Lock.unlock()}.
The Lock Checker enforces that any expression whose type implements
\sunjavadoc{java.base/java/util/concurrent/locks/Lock.html}{Lock} is used as an
explicit lock, and all other expressions are used as monitor locks.
% The class that implements the Lock interface could itself use the
% current object as a monitor lock. This doesn't seem like it
% needs to be mentioned here, though.
Ensuring that your program obeys its locking discipline is an easy and
effective way to eliminate a common and important class of errors.
If the Lock Checker issues no warnings, then your program obeys its locking discipline.
However, your program might still have other types of concurrency errors.
%
For example, you might have specified an inadequate locking discipline
because you forgot some \refqualclass{checker/lock/qual}{GuardedBy}
annotations.
%
Your program might release and
re-acquire the lock, when correctness requires it to hold it throughout a
computation.
%
And, there are other concurrency errors that cannot, or
should not, be solved with locks.
\sectionAndLabel{Lock annotations}{lock-annotations}
This section describes the lock annotations you can write on types and methods.
\subsectionAndLabel{Type qualifiers}{lock-type-qualifiers}
\begin{description}
\item[\refqualclass{checker/lock/qual}{GuardedBy}{\small(\emph{exprSet})}]
If a variable \<x> has type \<@GuardedBy("\emph{expr}")>, then a thread may
dereference the value referred to by \<x> only when the thread holds the
lock that \emph{expr} currently evaluates to.
The \<@GuardedBy> annotation can list multiple expressions, as in
\<@GuardedBy(\ttlcb"\emph{expr1}", "\emph{expr2}"\ttrcb)>, in which case
the dereference is
permitted only if the thread holds all the locks.
Section~\ref{java-expressions-as-arguments} explains which
expressions the Lock Checker is able to analyze as lock expressions.
These include \code{<self>}, i.e. the value of the annotated reference
(non-primitive) variable. For example, \code{@GuardedBy("<self>") Object o}
indicates that the value referenced by \<o> is guarded by the intrinsic
(monitor) lock of the value referenced by \<o>.
\<@GuardedBy(\{\})>, which means the value is always allowed to be
dereferenced, is the default type qualifier that is used for all locations
where the programmer does not
write an explicit locking type qualifier (except all CLIMB-to-top locations
other than upper bounds and exception parameters --- see Section~\ref{climb-to-top}).
(Section~\ref{lock-checker-default-qualifier} discusses this choice.)
It is also the conservative
default type qualifier for method parameters in unannotated libraries
(see \chapterpageref{annotating-libraries}).
\item[\refqualclass{checker/lock/qual}{GuardedByUnknown}]
If a variable \<x> has type \code{@GuardedByUnknown}, then
it is not known which locks protect \<x>'s value. Those locks might
even be out of scope (inaccessible) and therefore unable to be written
in the annotation.
The practical consequence is that
the value referred to by \<x> can never be dereferenced.
Any value can be assigned to a variable of type
\code{@GuardedByUnknown}. In particular, if it is written on a
formal parameter, then any value,
including one whose locks are not currently held,
may be passed as an argument.
\<@GuardedByUnknown> is the conservative
default type qualifier for method receivers in unannotated libraries
(see \chapterpageref{annotating-libraries}).
\item[\refqualclass{checker/lock/qual}{GuardedByBottom}]
If a variable \<x> has type \code{@GuardedByBottom}, then
the value referred to by \<x> is \code{null} and can never
be dereferenced.
\end{description}
\begin{figure}
\includeimage{lock-guardedby}{3cm}
\caption{The subtyping relationship of the Lock Checker's qualifiers.
\code{@GuardedBy(\{\})} is the default type qualifier for unannotated
types (except all CLIMB-to-top locations other than upper bounds and exception
parameters --- see Section~\ref{climb-to-top}).
}
\label{fig-lock-guardedby-hierarchy}
\end{figure}
Figure~\ref{fig-lock-guardedby-hierarchy} shows the type hierarchy of these
qualifiers.
All \code{@GuardedBy} annotations are incomparable:
if \emph{exprSet1} $\neq$ \emph{exprSet2}, then \code{@GuardedBy(\emph{exprSet1})} and
\code{@GuardedBy(\emph{exprSet2})} are siblings in the type hierarchy.
You might expect that
\<@GuardedBy(\{"x", "y"\}) T> is a subtype of \<@GuardedBy(\{"x"\}) T>. The
first type requires two locks to be held, and the second requires only one
lock to be held and so could be used in any situation where both locks are
held. The type system conservatively prohibits this in order to prevent
type-checking loopholes that would result from aliasing and side effects
--- that is, from having two mutable references, of different types, to the
same data. See
Section~\ref{lock-guardedby-invariant-subtyping} for an example
of a problem that would occur if this rule were relaxed.
\paragraphAndLabel{Polymorphic type qualifiers}{lock-polymorphic-type-qualifiers}
%\refqualclass{checker/lock/qual}{GuardSatisfied}{\small(\emph{index})}
%and
%\refqualclass{checker/interning/qual}{PolyGuardedBy}
%indicates qualifier polymorphism. For a description of qualifier
%polymorphism, see Section~\ref{qualifier-polymorphism}.
\begin{description}
\item[\refqualclass{checker/lock/qual}{GuardSatisfied}{\small(\emph{index})}]
If a variable \<x> has type \code{@GuardSatisfied}, then all
lock expressions for \<x>'s value are held.
As with other qualifier-polymorphism annotations
(Section~\ref{qualifier-polymorphism}), the \emph{index} argument
indicates when two values are guarded by the same (unknown) set of locks.
\code{@GuardSatisfied} is only allowed in method signatures: on
formal parameters (including the receiver) and return types.
It may not be written on fields. Also, it is a limitation of the
current design that \code{@GuardSatisfied} may not be written on
array elements or on local variables.
A return type can only be annotated with \<@GuardSatisfied(index)>,
not \<@GuardSatisfied>.
See Section~\ref{lock-checker-polymorphism-example}
for an example of a use of \code{@GuardSatisfied}.
%\item[\refqualclass{checker/interning/qual}{PolyGuardedBy}]
% It is unknown what the guards are or whether they are held.
% An expression whose type is \code{@PolyGuardedBy}
% cannot be dereferenced.
\end{description}
\subsectionAndLabel{Declaration annotations}{lock-declaration-annotations}
The Lock Checker supports several annotations that specify method behavior.
These are declaration annotations, not type annotations: they apply to the
method itself rather than to some particular type.
\paragraphAndLabel{Method pre-conditions and post-conditions}{lock-method-pre-post-conditions}
\begin{sloppypar}
\begin{description}
\item[\refqualclass{checker/lock/qual}{Holding}\small{(String[] locks)}]
All the given lock expressions
are held at the method call site.
\item[\refqualclass{checker/lock/qual}{EnsuresLockHeld}\small{(String[] locks)}]
The given lock
expressions are
locked upon method return if the method
terminates successfully. This is useful for annotating a
method that acquires a lock such as
\sunjavadoc{java.base/java/util/concurrent/locks/ReentrantLock.html\#lock()}{ReentrantLock.lock()}.
\item[\refqualclass{checker/lock/qual}{EnsuresLockHeldIf}\small{(String[] locks, boolean result)}]
If the annotated method returns the given
boolean value (true or false), the given lock
expressions are locked upon method return if the method
terminates successfully.
This is useful for annotating a
method that conditionally acquires a lock.
See Section~\ref{ensureslockheld-examples} for examples.
\end{description}
\paragraphAndLabel{Side effect specifications}{lock-side-effect-specifications}
\begin{description}
\item[\refqualclass{checker/lock/qual}{LockingFree}]
The method does not acquire or release locks,
directly or indirectly. The method is not \<synchronized>, it contains
no \<synchronized> blocks, it contains no calls to \<lock> or \<unlock>
methods, and it contains no calls to methods that are not themselves \<@LockingFree>.
Since
\code{@SideEffectFree} implies \code{@LockingFree}, if both are applicable
then you only need to write \code{@SideEffectFree}.
\item[\refqualclass{checker/lock/qual}{ReleasesNoLocks}]
The method maintains a strictly nondecreasing lock hold count on the
current thread for any locks that were held prior
to the method call. The method might acquire locks but then release
them, or might acquire locks but not release them (in which case it should
also be annotated with
\refqualclass{checker/lock/qual}{EnsuresLockHeld} or
\refqualclass{checker/lock/qual}{EnsuresLockHeldIf}).
This is the default for methods being type-checked that have no \<@LockingFree>,
\<@MayReleaseLocks>, \code{@SideEffectFree}, or \code{@Pure}
annotation.
\item[\refqualclass{checker/lock/qual}{MayReleaseLocks}]
The method may release locks that were held prior to the method being called.
You can write this when you are certain the method releases locks, or
when you don't know whether the method releases locks.
This is the conservative default for methods in unannotated libraries (see \chapterpageref{annotating-libraries}).
\end{description}
\end{sloppypar}
\sectionAndLabel{Type-checking rules}{lock-type-checking-rules}
In addition to the standard subtyping rules enforcing the subtyping relationship
described in Figure~\ref{fig-lock-guardedby-hierarchy}, the Lock Checker enforces
the following additional rules.
\subsectionAndLabel{Polymorphic qualifiers}{lock-type-checking-rules-polymorphic-qualifiers}
\begin{description}
\item[\code{@GuardSatisfied}]
The overall rules for polymorphic qualifiers are given in
Section~\ref{qualifier-polymorphism}.
Here are additional constraints for (pseudo-)assignments:
\begin{itemize}
\item
If the left-hand side has type \<@GuardSatisfied> (with or without an index),
then all locks mentioned in the right-hand side's \<@GuardedBy> type
must be currently held.
\item
A formal parameter with type qualifier \<@GuardSatisfied> without an
index cannot be assigned to.
\item
If the left-hand side is a formal parameter with type
\<@GuardSatisfied(\emph{index})>, the right-hand-side must have
identical \<@GuardSatisfied(\emph{index})> type.
\end{itemize}
If a formal parameter type is
annotated with \<@GuardSatisfied> without an index, then that formal parameter
type is unrelated to every other type in the \<@GuardedBy> hierarchy,
including other occurrences of \<@GuardSatisfied> without an index.
\<@GuardSatisfied> may not be used on formal parameters, receivers, or
return types of a method annotated with \<@MayReleaseLocks>.
\end{description}
\subsectionAndLabel{Dereferences}{lock-type-checking-rules-dereferences}
\begin{description}
\item[\code{@GuardedBy}]
An expression of type \<@GuardedBy(\emph{eset})> may be dereferenced only
if all locks in \emph{eset} are held.
\item[\code{@GuardSatisfied}]
An expression of type \<@GuardSatisfied> may be dereferenced.
\item[Not \code{@GuardedBy} or \code{@GuardSatisfied}]
An expression whose type is not annotated with \code{@GuardedBy} or
\code{@GuardSatisfied} may not be dereferenced.
% In particular, an expression of type \code{@PolyGuardedBy} may not be dereferenced.
\end{description}
\subsectionAndLabel{Primitive types, boxed primitive types, and Strings}{lock-type-checking-rules-primitives}
Primitive types, boxed primitive types (such as \<java.lang.Integer>), and type \<java.lang.String>
are annotated with \<@GuardedBy(\{\})>.
It is an error for the programmer to annotate any of these types with an annotation from
the \<@GuardedBy> type hierarchy, including \<@GuardedBy(\{\})>.
% Primitive values are not guarded. Instead, the variables that store them are.
% Therefore, for reads, writes and other operations on primitive values, the Lock Checker requires that
% the appropriate locks be held, but it does not enforce any other rules.
% In particular, it does not require the annotations
% in the types involved in the operation (including assignments and
% pseudo-assignments) to match. For example, given:
% \begin{verbatim}
% ReentrantLock lock1, lock2;
% @GuardedBy("lock1") int a;
% @GuardedBy("lock2") int b;
% @GuardedBy({}) int c;
% ...
% lock1.lock();
% lock2.lock();
% a = b;
% a = c;
% a = b + c;
% \end{verbatim}
% The expressions \code{a = b}, \code{a = c}, and \code{a = b + c}
% all type check, whereas none of them would type check if \code{a},
% \code{b} and \code{c} were not primitives.
\subsectionAndLabel{Overriding}{lock-type-checking-rules-overriding}
\begin{description}
\item[Overriding methods annotated with \code{@Holding}]
If class $B$ overrides method $m$ from class $A$, then the expressions in
$B$'s \<@Holding>
annotation must be a subset of or equal to that of $A$'s \<@Holding>
annotation.
\item[Overriding methods annotated with side effect annotations]
If class $B$ overrides method $m$ from class $A$, then
the side effect annotation on $B$'s declaration of $m$
must be at least as strong as that in $A$'s declaration of $m$.
From weakest to strongest, the side effect annotations
processed by the Lock Checker are:
\begin{verbatim}
@MayReleaseLocks
@ReleasesNoLocks
@LockingFree
@SideEffectFree
@Pure
\end{verbatim}
\end{description}
\subsectionAndLabel{Side effects}{lock-type-checking-rules-polymorphic-side-effects}
\begin{description}
\item[Releasing explicit locks]
Any method that releases an explicit lock must be annotated
with \code{@MayReleaseLocks}.
The Lock Checker issues a warning if it encounters a method declaration
annotated with \code{@MayReleaseLocks} and having a formal parameter
or receiver annotated with \code{@GuardSatisfied}. This is because
the Lock Checker cannot guarantee that the guard will be satisfied
throughout the body of a method if that method may release a lock.
\item[No side effects on lock expressions]
If expression \emph{expr} is used to acquire a lock, then
\emph{expr} must evaluate to the same value, starting from when
\emph{expr} is used to acquire a lock until \emph{expr} is used to
release the lock.
An expression is used to acquire a lock if it is the receiver at a
call site of a \<synchronized> method, is the expression in a
\<synchronized> block, or is the argument to a \<lock> method.
\item[Locks are released after possible side effects]
% These are standard dataflow analysis rules, but are worth
% repeating here due to how important they are for the day-to-day
% use of the Lock Checker. I believe this would be the single
% largest source of confusion amongst Lock Checker users if this
% were not stated explicitly.
After a call to a method annotated with \code{@LockingFree},
\code{@ReleasesNoLocks}, \code{@SideEffectFree}, or \code{@Pure},
the Lock Checker's estimate of held locks
after a method call is the same as that prior to the method call.
After a call to a method annotated with \code{@MayReleaseLocks},
the estimate of held locks is conservatively reset to the empty set,
except for those locks specified to be held after the call
by an \code{@EnsuresLockHeld} or \code{@EnsuresLockHeldIf}
annotation on the method. Assignments to variables also
cause the estimate of held locks to be conservatively reduced
to a smaller set if the Checker Framework determines that the
assignment might have side-effected a lock expression.
For more information on side effects, please refer to
Section~\ref{type-refinement-purity}.
\end{description}
\sectionAndLabel{Examples}{lock-examples}
The Lock Checker guarantees that a value that was computed from an expression of \code{@GuardedBy} type is
dereferenced only when the current thread holds all the expressions in the
\code{@GuardedBy} annotation.
\subsectionAndLabel{Examples of @GuardedBy}{lock-examples-guardedby}
The following example demonstrates the basic
type-checking rules.
\begin{Verbatim}
class MyClass {
final ReentrantLock lock; // Initialized in the constructor
@GuardedBy("lock") Object x = new Object();
@GuardedBy("lock") Object y = x; // OK, since dereferences of y will require "lock" to be held.
@GuardedBy({}) Object z = x; // ILLEGAL since dereferences of z don't require "lock" to be held.
@GuardedBy("lock") Object myMethod() { // myMethod is implicitly annotated with @ReleasesNoLocks.
return x; // OK because the return type is annotated with @GuardedBy("lock")
}
[...]
void exampleMethod() {
x.toString(); // ILLEGAL because the lock is not known to be held
y.toString(); // ILLEGAL because the lock is not known to be held
myMethod().toString(); // ILLEGAL because the lock is not known to be held
lock.lock();
x.toString(); // OK: the lock is known to be held
y.toString(); // OK: the lock is known to be held, and toString() is annotated with @SideEffectFree.
myMethod().toString(); // OK: the lock is known to be held, since myMethod
// is implicitly annotated with @ReleasesNoLocks.
}
}
\end{Verbatim}
Note that the expression \code{new Object()} is inferred to have type \code{@GuardedBy("lock")}
because it is immediately assigned to a newly-declared
variable having type annotation \code{@GuardedBy("lock")}. You could
explicitly write \code{new @GuardedBy("lock") Object()} but it is not
required.
The following example demonstrates that using \code{<self>} as a lock expression
allows a guarded value to be dereferenced even when the original
variable name the value was originally assigned to falls out of scope.
\begin{Verbatim}
class MyClass {
private final @GuardedBy("<self>") Object x = new Object();
void method() {
x.toString(); // ILLEGAL because x is not known to be held.
synchronized(x) {
x.toString(); // OK: x is known to be held.
}
}
public @GuardedBy("<self>") Object get_x() {
return x; // OK, since the return type is @GuardedBy("<self>").
}
}
class MyOtherClass {
void method() {
MyClass m = new MyClass();
final @GuardedBy("<self>") Object o = m.get_x();
o.toString(); // ILLEGAL because o is not known to be held.
synchronized(o) {
o.toString(); // OK: o is known to be held.
}
}
}
\end{Verbatim}
\subsectionAndLabel{@GuardedBy(\{``a'', ``b''\}) is not a subtype of @GuardedBy(\{``a''\})}{lock-guardedby-invariant-subtyping}
\textbf{@GuardedBy(exprSet)}
The following example demonstrates the reason the Lock Checker enforces the
following rule: if \emph{exprSet1} $\neq$ \emph{exprSet2}, then
\code{@GuardedBy(\emph{exprSet1})} and \code{@GuardedBy(\emph{exprSet2})} are siblings in the type
hierarchy.
\begin{Verbatim}
class MyClass {
final Object lockA = new Object();
final Object lockB = new Object();
@GuardedBy("lockA") Object x = new Object();
@GuardedBy({"lockA", "lockB"}) Object y = new Object();
void myMethod() {
y = x; // ILLEGAL; if legal, later statement x.toString() would cause trouble
synchronized(lockA) {
x.toString(); // dereferences y's value without holding lock lockB
}
}
}
\end{Verbatim}
If the Lock Checker permitted the assignment
\code{y = x;}, then the undesired dereference would be possible.
\subsectionAndLabel{Examples of @Holding}{lock-examples-holding}
The following example shows the interaction between \<@GuardedBy> and
\<@Holding>:
\begin{Verbatim}
void helper1(@GuardedBy("myLock") Object a) {
a.toString(); // ILLEGAL: the lock is not held
synchronized(myLock) {
a.toString(); // OK: the lock is held
}
}
@Holding("myLock")
void helper2(@GuardedBy("myLock") Object b) {
b.toString(); // OK: the lock is held
}
void helper3(@GuardedBy("myLock") Object d) {
d.toString(); // ILLEGAL: the lock is not held
}
void myMethod2(@GuardedBy("myLock") Object e) {
helper1(e); // OK to pass to another routine without holding the lock
// (but helper1's body has an error)
e.toString(); // ILLEGAL: the lock is not held
synchronized (myLock) {
helper2(e); // OK: the lock is held
helper3(e); // OK, but helper3's body has an error
}
}
\end{Verbatim}
\subsectionAndLabel{Examples of @EnsuresLockHeld and @EnsuresLockHeldIf}{ensureslockheld-examples}
\code{@EnsuresLockHeld} and \code{@EnsuresLockHeldIf} are primarily intended
for annotating JDK locking methods, as in:
\begin{Verbatim}
package java.util.concurrent.locks;
class ReentrantLock {
@EnsuresLockHeld("this")
public void lock();
@EnsuresLockHeldIf (expression="this", result=true)
public boolean tryLock();
...
}
\end{Verbatim}
They can also be used to annotate user methods, particularly for
higher-level lock constructs such as a Monitor, as in this simplified example:
\begin{Verbatim}
public class Monitor {
private final ReentrantLock lock; // Initialized in the constructor
...
@EnsuresLockHeld("lock")
public void enter() {
lock.lock();
}
...
}
\end{Verbatim}
\subsectionAndLabel{Example of @LockingFree, @ReleasesNoLocks, and @MayReleaseLocks}{lock-lockingfree-example}
\code{@LockingFree} is useful when a method does not make any use of synchronization
or locks but causes other side effects (hence \code{@SideEffectFree} is not appropriate).
\code{@SideEffectFree} implies \code{@LockingFree}, therefore if both are applicable,
you should only write \code{@SideEffectFree}. \code{@ReleasesNoLocks} has a weaker guarantee
than \code{@LockingFree}, and \code{@MayReleaseLocks} provides no guarantees.
\begin{verbatim}
private Object myField;
private final ReentrantLock lock; // Initialized in the constructor
private @GuardedBy("lock") Object x; // Initialized in the constructor
[...]
// This method does not use locks or synchronization, but it cannot
// be annotated as @SideEffectFree since it alters myField.
@LockingFree
void myMethod() {
myField = new Object();
}
@SideEffectFree
int mySideEffectFreeMethod() {
return 0;
}
@MayReleaseLocks
void myUnlockingMethod() {
lock.unlock();
}
@ReleasesNoLocks
void myLockingMethod() {
lock.lock();
}
@MayReleaseLocks
void clientMethod() {
if (lock.tryLock()) {
x.toString(); // OK: the lock is held
myMethod();
x.toString(); // OK: the lock is still held since myMethod is locking-free
mySideEffectFreeMethod();
x.toString(); // OK: the lock is still held since mySideEffectFreeMethod is side-effect-free
myUnlockingMethod();
x.toString(); // ILLEGAL: myUnlockingMethod may have released a lock
}
if (lock.tryLock()) {
x.toString(); // OK: the lock is held
myLockingMethod();
x.toString(); // OK: the lock is held
}
if (lock.isHeldByCurrentThread()) {
x.toString(); // OK: the lock is known to be held
}
}
\end{verbatim}
\subsectionAndLabel{Polymorphism and method formal parameters with unknown guards}{lock-checker-polymorphism-example}
The polymorphic \code{@GuardSatisfied} type annotation allows a method body
to dereference the method's formal parameters even if the
\code{@GuardedBy} annotations on the actual parameters are unknown at
the method declaration site.
The declaration of
\sunjavadoc{java.base/java/lang/StringBuffer.html\#append(java.lang.String)}{StringBuffer.append(String str)}
is annotated as:
\begin{verbatim}
@LockingFree
public @GuardSatisfied(1) StringBuffer append(@GuardSatisfied(1) StringBuffer this,
@GuardSatisfied(2) String str)
\end{verbatim}
The method manipulates the values of its arguments, so all their locks must
be held. However, the declaration does not know what those are and they
might not even be in scope at the declaration. Therefore, the declaration
cannot use \<@GuardedBy> and must use \<@GuardSatisfied>. The arguments to
\<@GuardSatisfied> indicate that the receiver and result (which are the
same value) are guarded by the same (unknown, possibly empty) set of locks,
and the \<str> parameter may be guarded by a different set of locks.
The \code{@LockingFree} annotation indicates that
this method makes no use of
locks or synchronization.
Given these annotations on \<append>, the following code type-checks:
\begin{verbatim}
final ReentrantLock lock1, lock2; // Initialized in the constructor
@GuardedBy("lock1") StringBuffer filename;
@GuardedBy("lock2") StringBuffer extension;
...
lock1.lock();
lock2.lock();
filename = filename.append(extension);
\end{verbatim}
% The 'filename = ' assignment is unnecessary in the example
% and is not good Java style, but it illustrates the type-checking against the
% return value of the call to append.
\sectionAndLabel{More locking details}{lock-details}
This section gives some details that are helpful for understanding how Java
locking and the Lock Checker works.
\subsectionAndLabel{Two types of locking: monitor locks and explicit locks}{lock-two-types}
Java provides two types of locking: monitor locks and explicit locks.
\begin{itemize}
\item
A \<synchronized(\emph{E})> block acquires the lock on the value of
\emph{E}; similarly, a method declared using the \<synchronized> method
modifier acquires the lock on the method receiver when called.
(More precisely,
the current thread locks the monitor associated with the value of
\emph{E}; see \href{https://docs.oracle.com/javase/specs/jls/se11/html/jls-17.html#jls-17.1}{JLS \S17.1}.)
The lock is automatically released when execution exits the block or the
method body, respectively.
We use the term ``monitor lock'' for a lock acquired using a
\<synchronized> block or \<synchronized> method modifier.
\item A method call, such as
\sunjavadoc{java.base/java/util/concurrent/locks/Lock.html\#lock()}{Lock.lock()},
acquires a lock that implements the
\sunjavadoc{java.base/java/util/concurrent/locks/Lock.html}{Lock}
interface.
The lock is released by another method call, such as
\sunjavadoc{java.base/java/util/concurrent/locks/Lock.html\#unlock()}{Lock.unlock()}.
We use the term ``explicit lock'' for a lock expression acquired in this
way.
\end{itemize}
You should not mix the two varieties of locking, and the Lock Checker
enforces this. To prevent an object from being used both as a monitor and
an explicit lock, the Lock Checker issues a warning if a
\<synchronized(\emph{E})> block's expression \<\emph{E}> has a type that
implements \sunjavadoc{java.base/java/util/concurrent/locks/Lock.html}{Lock}.
% The Lock Checker does not keep track of which locks are monitors
% and which are explicit, so this check is necessary for the Lock Checker to
% function correctly, and it also alerts the programmer of a code smell.
\subsectionAndLabel{Held locks and held expressions; aliasing}{lock-aliasing}
Whereas Java locking is defined in terms of values, Java programs are
written in terms of expressions.
We say that a lock expression is held if the value to which the expression
currently evaluates is held.
The Lock Checker conservatively estimates the expressions that are held at
each point in a program.
The Lock Checker does not track aliasing
(different expressions that evaluate to the same value); it only considers
the exact expression used to acquire a lock to be held. After any statement
that might side-effect a held expression or a lock expression, the Lock
Checker conservatively considers the expression to be no longer held.
Section~\ref{java-expressions-as-arguments} explains which Java
expressions the Lock Checker is able to analyze as lock expressions.
The \code{@LockHeld} and \code{@LockPossiblyHeld} type qualifiers are used internally by the Lock Checker
and should never be written by the programmer.
If you
see a warning mentioning \code{@LockHeld} or \code{@LockPossiblyHeld},
please contact the Checker Framework developers as it is likely to
indicate a bug in the Checker Framework.
\subsectionAndLabel{Run-time checks for locking}{lock-runtime-checks}
When you perform a run-time check for locking, such as
\<if (explicitLock.isHeldByCurrentThread())\{...\}> or
\<if (Thread.holdsLock(monitorLock))\{...\}>,
then the Lock Checker considers the lock expression to be held
within the scope of the test. For more details, see
Section~\ref{type-refinement}.
% Note that the java.util.concurrent.locks.Lock interface does not include
% a run-time test, but ReentrantLock does.
\subsectionAndLabel{Discussion of default qualifier}{lock-checker-default-qualifier}
The default qualifier for unannotated types is \<@GuardedBy(\{\})>.
This default forces you to write explicit \<@GuardSatisfied> in method
signatures in the common case that clients ensure that all locks are held.
It might seem that \<@GuardSatisfied> would be a better default for
method signatures, but such a default would require even more annotations.
The reason is that \<@GuardSatisfied> cannot be used on fields. If
\<@GuardedBy(\{\})> is the default for fields but \<@GuardSatisfied> is the
default for parameters and return types, then getters, setters, and many
other types of methods do not type-check without explicit lock qualifiers.
\subsectionAndLabel{Discussion of \<@Holding>}{lock-checker-holding}
A programmer might choose to use the \code{@Holding} method annotation in
two different ways: to specify correctness constraints for a
synchronization protocol, or to summarize intended usage. Both of these
approaches are useful, and the Lock Checker supports both.
\paragraphAndLabel{Synchronization protocol}{lock-checker-holding-synchronization-protocol}
\code{@Holding} can specify a synchronization protocol that
is not expressible as locks over the parameters to a method. For example, a global lock
or a lock on a different object might need to be held. By requiring locks to be
held, you can create protocol primitives without giving up
the benefits of the annotations and checking of them.
\paragraphAndLabel{Method summary that simplifies reasoning}{lock-checker-holding-method-summary}
\code{@Holding} can be a method summary that simplifies reasoning. In
this case, the \code{@Holding} doesn't necessarily introduce a new
correctness constraint; the program might be correct even if the lock
were not already acquired.
Rather, here \code{@Holding} expresses a fact about execution: when
execution reaches this point, the following locks are known to be already held. This
fact enables people and tools to reason intra- rather than
inter-procedurally.
In Java, it is always legal to re-acquire a lock that is already held,
and the re-acquisition always works. Thus, whenever you write
\begin{Verbatim}
@Holding("myLock")
void myMethod() {
...
}
\end{Verbatim}
\noindent
it would be equivalent, from the point of view of which locks are held
during the body, to write
\begin{Verbatim}
void myMethod() {
synchronized (myLock) { // no-op: re-acquire a lock that is already held
...
}
}
\end{Verbatim}
It is better to write a \code{@Holding} annotation rather than writing the
extra synchronized block. Here are reasons:
\begin{itemize}
\item
The annotation documents the fact that the lock is intended to already be
held; that is, the method's contract requires that the lock be held when
the method is called.
\item
The Lock Checker enforces that the lock is held when the method is
called, rather than masking a programmer error by silently re-acquiring
the lock.
\item
The version with a synchronized statement can deadlock if, due to a programmer error,
the lock is not already held. The Lock Checker prevents this type of
error.
\item
The annotation has no run-time overhead. The lock re-acquisition
consumes time, even if it succeeds.
\end{itemize}
\sectionAndLabel{Other lock annotations}{lock-other-annotations}
The Checker Framework's lock annotations are similar to annotations used
elsewhere.
If your code is already annotated with a different lock
annotation, the Checker Framework can type-check your code.
It treats annotations from other tools
as if you had written the corresponding annotation from the
Lock Checker, as described in Figure~\ref{fig-lock-refactoring}.
If the other annotation is a declaration annotation, it may be moved; see
Section~\ref{declaration-annotations-moved}.
% These lists should be kept in sync with LockAnnotatedTypeFactory.java .
\begin{figure}
\begin{center}
% The ~ around the text makes things look better in Hevea (and not terrible
% in LaTeX).
\begin{tabular}{ll}
\begin{tabular}{|l|}
\hline
~net.jcip.annotations.GuardedBy~ \\ \hline
~javax.annotation.concurrent.GuardedBy~ \\ \hline
\end{tabular}
&
$\Rightarrow$
%HEVEA ~org.checkerframework.checker.lock.qual.GuardedBy (for fields) or \ldots Holding (for methods)~
%BEGIN LATEX
\begin{tabular}{l}
~org.checkerframework.checker.lock.qual.GuardedBy (for fields), or~ \\
~org.checkerframework.checker.lock.qual.Holding (for methods)~
\end{tabular}
%END LATEX
\end{tabular}
\end{center}
%BEGIN LATEX
\vspace{-1.5\baselineskip}
%END LATEX
\caption{Correspondence between other lock annotations and the
Checker Framework's annotations.}
\label{fig-lock-refactoring}
\end{figure}
\subsectionAndLabel{Relationship to annotations in \emph{Java Concurrency in Practice}}{lock-jcip-annotations}
The book \href{http://jcip.net/}{\emph{Java Concurrency in Practice}}~\cite{Goetz2006} defines a
\href{http://jcip.net.s3-website-us-east-1.amazonaws.com/annotations/doc/net/jcip/annotations/GuardedBy.html}{\code{@GuardedBy}} annotation that is the inspiration for ours. The book's
\code{@GuardedBy} serves two related but distinct purposes:
\begin{itemize}
\item
When applied to a field, it means that the given lock must be held when
accessing the field. The lock acquisition and the field access may occur
arbitrarily far in the future.
\item
When applied to a method, it means that the given lock must be held by
the caller at the time that the method is called --- in other words, at
the time that execution passes the \code{@GuardedBy} annotation.
\end{itemize}
The Lock Checker renames the method annotation to
\refqualclass{checker/lock/qual}{Holding}, and it generalizes the
\refqualclass{checker/lock/qual}{GuardedBy} annotation into a type annotation
that can apply not just to a field but to an arbitrary type (including the
type of a parameter, return value, local variable, generic type parameter,
etc.). Another important distinction is that the Lock Checker's
annotations express and enforce a locking discipline over values, just like
the JLS expresses Java's locking semantics; by contrast, JCIP's annotations
express a locking discipline that protects variable names and does not
prevent race conditions.
This makes the annotations more expressive and also more amenable
to automated checking. It also accommodates the distinct
meanings of the two annotations, and resolves ambiguity when \<@GuardedBy>
is written in a location that might apply to either the method or the
return type.
(The JCIP book gives some rationales for reusing the annotation name for
two purposes. One rationale is
that there are fewer annotations to learn. Another rationale is
that both variables and methods are ``members'' that can be ``accessed''
and \code{@GuardedBy} creates preconditions for doing so.
Variables can be accessed by reading or writing them (putfield, getfield),
and methods can be accessed by calling them (invokevirtual,
invokeinterface). This informal intuition is
inappropriate for a tool that requires precise semantics.)
% It would not work to retain the name \code{@GuardedBy} but put it on the
% receiver; an annotation on the receiver indicates what lock must be held
% when it is accessed in the future, not what must have already been held
% when the method was called.
\sectionAndLabel{Possible extensions}{lock-extensions}
The Lock Checker validates some uses of locks, but not all. It would be
possible to enrich it with additional annotations. This would increase the
programmer annotation burden, but would provide additional guarantees.
Lock ordering: Specify that one lock must be acquired before or after
another, or specify a global ordering for all locks. This would prevent
deadlock.
Not-holding: Specify that a method must not be called if any of the listed
locks are held.
These features are supported by
\href{http://clang.llvm.org/docs/ThreadSafetyAnalysis.html}{Clang's
thread-safety analysis}.
% LocalWords: quals GuardedBy JCIP putfield getfield invokevirtual
% LocalWords: invokeinterface threadsafety Clang's GuardedByUnknown
% LocalWords: api 5cm lockexpr Dereferencing exprSet expr expr1 expr2
% LocalWords: GuardedByBottom exprSet1 exprSet2 GuardSatisfied 3cm pre
% LocalWords: PolyGuardedBy EnsuresLockHeld ReentrantLock boolean eset
% LocalWords: EnsuresLockHeldIf LockingFree ReleasesNoLocks str lock1
% LocalWords: MayReleaseLocks GuardedByName lock2 jls JLS LockHeld intra
% LocalWords: LockPossiblyHeld explicitLock isHeldByCurrentThread JCIP's
% LocalWords: holdsLock monitorLock cleanroom AconcurrentSemantics
|