Index: doc/proposals/concurrency/concurrency.tex
===================================================================
--- doc/proposals/concurrency/concurrency.tex	(revision 03bb816f896612125c8f1acd78ef46603e99f236)
+++ doc/proposals/concurrency/concurrency.tex	(revision ffc9f5a7c031fc9030b12c8b0ca2d84dc9cd6d78)
@@ -350,155 +350,308 @@
 
 \subsection{Internal scheduling} \label{insched}
-Monitors also need to schedule waiting threads internally as a mean of synchronization. Internal scheduling is one of the simple examples of such a feature. It allows users to declare condition variables and have threads wait and signaled from them. Here is a simple example of such a technique :
-
-\begin{lstlisting}
-	mutex struct A {
-		condition e;
-	}
-
-	void foo(A & mutex a) {
-		//...
-		wait(a.e);
-		//...
-	}
-
-	void bar(A & mutex a) {
-		signal(a.e);
-	}
-\end{lstlisting}
-
-Note that in \CFA, \code{condition} have no particular need to be stored inside a monitor, beyond any software engineering reasons. Here routine \code{foo} waits for the \code{signal} from \code{bar} before making further progress, effectively ensuring a basic ordering. 
-
-As for simple mutual exclusion, these semantics must also be extended to include \gls{group-acquire} :
+
 \begin{center}
 \begin{tabular}{ c @{\hskip 0.65in} c }
-Thread 1 & Thread 2 \\
-\begin{lstlisting}
-void foo(A & mutex a,
-           A & mutex b) {
-	//...
-	wait(a.e);
-	//...
-}
-
-foo(a, b);
-\end{lstlisting} &\begin{lstlisting}
-void bar(A & mutex a,
-           A & mutex b) {
-	signal(a.e);
-}
-
-
-
-bar(a, b);
+\begin{lstlisting}[language=Pseudo]
+acquire A
+	wait A
+release A
+\end{lstlisting}&\begin{lstlisting}[language=Pseudo]
+acquire A
+	signal A
+release A
 \end{lstlisting}
 \end{tabular}
 \end{center}
 
-To define the semantics of internal scheduling, it is important to look at nesting and \gls{group-acquire}. Indeed, beyond concerns about lock ordering, without scheduling the two following pseudo codes are mostly equivalent. In fact, if we assume monitors are ordered alphabetically, these two pseudo codes would probably lead to exactly the same implementation :
-
-\begin{table}[h!]
-\centering
-\begin{tabular}{c c}
-\begin{lstlisting}[language=pseudo]
-monitor A, B, C
-
+Easy : like uC++
+
+\begin{center}
+\begin{tabular}{ c @{\hskip 0.65in} c }
+\begin{lstlisting}[language=Pseudo]
 acquire A
-	acquire B & C
-
-			//Do stuff
-
-	release B & C
+	acquire B
+		wait B
+	release B
 release A
-\end{lstlisting} &\begin{lstlisting}[language=pseudo]
-monitor A, B, C
-
+\end{lstlisting}&\begin{lstlisting}[language=Pseudo]
+acquire A
+	acquire B
+		signal B
+	release B
+release A
+\end{lstlisting}
+\end{tabular}
+\end{center}
+
+Also easy : like uC++
+
+\begin{center}
+\begin{tabular}{ c @{\hskip 0.65in} c }
+\begin{lstlisting}[language=Pseudo]
+acquire A & B
+	wait A & B
+release A & B
+\end{lstlisting}&\begin{lstlisting}[language=Pseudo]
+acquire A & B
+	signal A & B
+release A & B
+\end{lstlisting}
+\end{tabular}
+\end{center}
+
+Simplest extension : can be made like uC++ by tying B to A
+
+\begin{center}
+\begin{tabular}{ c @{\hskip 0.65in} c }
+\begin{lstlisting}[language=Pseudo]
+acquire A
+	// Code Section 1
+	acquire B
+		// Code Section 2
+		wait A & B
+		// Code Section 3
+	release B
+	// Code Section 4
+release A
+\end{lstlisting}&\begin{lstlisting}[language=Pseudo]
+acquire A
+	// Code Section 5
+	acquire B
+		// Code Section 6
+		signal A & B
+		// Code Section 7
+	release B
+	// Code Section 8
+release A
+\end{lstlisting}
+\end{tabular}
+\end{center}
+
+Hard extension :
+
+Incorrect options for the signal : 
+
+\begin{description}
+ \item[-] Release B and baton pass after Code Section 8 : Passing b without having it
+ \item[-] Keep B during Code Section 8 : Can lead to deadlocks since we secretly keep a lock longer than specified by the user
+ \item[-] Instead of release B transfer A and B to waiter then try to reacquire A before running Code Section 8 : This allows barging 
+\end{description}
+
+Since we don't want barging we need to pass A \& B and somehow block and get A back.
+
+\begin{center}
+\begin{tabular}{ c @{\hskip 0.65in} c }
+\begin{lstlisting}[language=Pseudo]
 acquire A
 	acquire B
 		acquire C
-			//Do stuff
-		release C
-	release B
-release A
+			wait A & B & C
+		1: release C
+	2: release B
+3: release A
+\end{lstlisting}&\begin{lstlisting}[language=Pseudo]
+acquire A
+	acquire B
+		acquire C
+			signal A & B & C
+		4: release C
+	5: release B
+6: release A
 \end{lstlisting}
 \end{tabular}
-\end{table}
-
-Once internal scheduling is introduce however, semantics of \gls{group-acquire} become relevant. For example, let us look into the semantics of the following pseudo-code :
-
+\end{center}
+
+To prevent barging :
+
+\begin{description}
+ \item[-] When the signaller hits 4 : pass A, B, C to waiter
+ \item[-] When the waiter hits 2 : pass A, B to signaller
+ \item[-] When the signaller hits 5 : pass A to waiter
+\end{description}
+
+
+\begin{center}
+\begin{tabular}{ c @{\hskip 0.65in} c }
 \begin{lstlisting}[language=Pseudo]
-1: monitor A, B, C
-2: condition c1
-3: 
-4: acquire A
-5: 		acquire A & B & C
-6: 				signal c1
-7: 		release A & B & C
-8: release A
-\end{lstlisting}
-
-Without \gls{group-acquire} signal simply baton passes the monitor lock on the next release. In the case above, we therefore need to indentify the next release. If line 8 is picked at the release point, then the signal will attempt to pass A \& B \& C, without having ownership of B \& C. Since this violates mutual exclusion, we conclude that line 7 is the only valid location where signalling can occur. The traditionnal meaning of signalling is to transfer ownership of the monitor(s) and immediately schedule the longest waiting task. However, in the discussed case, the signalling thread expects to maintain ownership of monitor A. This can be expressed in two differents ways : 1) the thread transfers ownership of all locks and reacquires A when it gets schedulled again or 2) it transfers ownership of all three monitors and then expects the ownership of A to be transferred back. 
-
-However, the question is does these behavior motivate supporting acquireing non-disjoint set of monitors. Indeed, if the previous example was modified to only acquire B \& C at line 5 (an release the accordingly) then in respects to scheduling, we could add the simplifying constraint that all monitors in a bulk will behave the same way, simplifying the problem back to a single monitor problem which has already been solved. For this constraint to be acceptble however, we need to demonstrate that in does not prevent any meaningful possibilities. And, indeed, we can look at the two previous interpretation of the above pseudo-code and conclude that supporting the acquiring of non-disjoint set of monitors does not add any expressiveness to the language.
-
-Option 1 reacquires the lock after the signal statement, this can be rewritten as follows without the need for non-disjoint sets :
-\begin{lstlisting}[language=Pseudo]
-monitor A, B, C
-condition c1
-
-acquire A & B & C
-	signal c1
-release A & B & C
 acquire A
-
-release A
-\end{lstlisting}
-
-This pseudo code has almost exaclty the same semantics as the code acquiring intersecting sets of monitors. 
-
-Option 2 uses two-way lock ownership transferring instead of reacquiring monitor A. Two-way monitor ownership transfer is normally done using signalBlock semantics, which immedietely transfers ownership of a monitor before getting the ownership back when the other thread no longer needs the monitor. While the example pseudo-code for Option 2 seems toe transfer ownership of A, B and C and only getting A back, this is not a requirement. Getting back all 3 monitors and releasing B and C differs only in performance. For this reason, the second option could arguably be rewritten as : 
-
-\begin{lstlisting}[language=Pseudo]
-monitor A, B, C
-condition c1
-
-acquire A
-	acquire B & C
-		signalBlock c1
-	release B & C
-release A
-\end{lstlisting}
-
-Obviously, the difference between these two snippets of pseudo code is that the first one transfers ownership of A, B and C while the second one only transfers ownership of B and C. However, this limitation can be removed by allowing user to release extra monitors when using internal scheduling, referred to as extended internal scheduling (pattent pending) from this point on. Extended internal scheduling means the two following pseudo-codes are functionnaly equivalent : 
-\begin{table}[h!]
-\centering
-\begin{tabular}{c @{\hskip 0.65in} c}
-\begin{lstlisting}[language=pseudo]
-monitor A, B, C
-condition c1
-
-acquire A
-	acquire B & C
-		signalBlock c1 with A
-	release B & C
-release A
-\end{lstlisting} &\begin{lstlisting}[language=pseudo]
-monitor A, B, C
-condition c1
-
-acquire A
-	acquire A & B & C
-		signal c1
-	release A & B & C
-release A
+	acquire C
+		acquire B
+			wait A & B & C
+		1: release B
+	2: release C
+3: release A
+\end{lstlisting}&\begin{lstlisting}[language=Pseudo]
+acquire B
+	acquire A
+		acquire C
+			signal A & B & C
+		4: release C
+	5: release A
+6: release B
 \end{lstlisting}
 \end{tabular}
-\end{table}
-
-It must be stated that the extended internal scheduling only makes sense when using wait and signalBlock, since they need to prevent barging, which cannot be done in the context of signal since the ownership transfer is strictly one-directionnal. 
-
-One critic that could arise is that extended internal schedulling is not composable since signalBlock must be explicitly aware of which context it is in. However, this argument is not relevant since acquire A, B and C in a context where a subset of them is already acquired cannot be achieved without spurriously releasing some locks or having an oracle aware of all monitors. Therefore, composability of internal scheduling is no more an issue than composability of monitors in general.
-
-The main benefit of using extended internal scheduling is that it offers the same expressiveness as intersecting monitor set acquiring but greatly simplifies the selection of a leader (or representative) for a group of monitor. Indeed, when using intersecting sets, it is not obvious which set intersects with other sets which means finding a leader representing only the smallest scope is a hard problem. Where as when using disjoint sets, any monitor that would be intersecting must be specified in the extended set, the leader can be chosen as any monitor in the primary set.
+\end{center}
+
+To prevent barging : When the signaller hits 4 : pass A, B, C to waiter. When the waiter hits 1 it must release B, 
+
+\begin{description}
+ \item[-] 
+ \item[-] When the waiter hits 1 : pass A, B to signaller
+ \item[-] When the signaller hits 5 : pass A, B to waiter
+ \item[-] When the waiter hits 2 : pass A to signaller
+\end{description}
+
+% Monitors also need to schedule waiting threads internally as a mean of synchronization. Internal scheduling is one of the simple examples of such a feature. It allows users to declare condition variables and have threads wait and signaled from them. Here is a simple example of such a technique :
+
+% \begin{lstlisting}
+% 	mutex struct A {
+% 		condition e;
+% 	}
+
+% 	void foo(A & mutex a) {
+% 		//...
+% 		wait(a.e);
+% 		//...
+% 	}
+
+% 	void bar(A & mutex a) {
+% 		signal(a.e);
+% 	}
+% \end{lstlisting}
+
+% Note that in \CFA, \code{condition} have no particular need to be stored inside a monitor, beyond any software engineering reasons. Here routine \code{foo} waits for the \code{signal} from \code{bar} before making further progress, effectively ensuring a basic ordering. 
+
+% As for simple mutual exclusion, these semantics must also be extended to include \gls{group-acquire} :
+% \begin{center}
+% \begin{tabular}{ c @{\hskip 0.65in} c }
+% Thread 1 & Thread 2 \\
+% \begin{lstlisting}
+% void foo(A & mutex a,
+%            A & mutex b) {
+% 	//...
+% 	wait(a.e);
+% 	//...
+% }
+
+% foo(a, b);
+% \end{lstlisting} &\begin{lstlisting}
+% void bar(A & mutex a,
+%            A & mutex b) {
+% 	signal(a.e);
+% }
+
+
+
+% bar(a, b);
+% \end{lstlisting}
+% \end{tabular}
+% \end{center}
+
+% To define the semantics of internal scheduling, it is important to look at nesting and \gls{group-acquire}. Indeed, beyond concerns about lock ordering, without scheduling the two following pseudo codes are mostly equivalent. In fact, if we assume monitors are ordered alphabetically, these two pseudo codes would probably lead to exactly the same implementation :
+
+% \begin{table}[h!]
+% \centering
+% \begin{tabular}{c c}
+% \begin{lstlisting}[language=pseudo]
+% monitor A, B, C
+
+% acquire A
+% 	acquire B & C
+
+% 			//Do stuff
+
+% 	release B & C
+% release A
+% \end{lstlisting} &\begin{lstlisting}[language=pseudo]
+% monitor A, B, C
+
+% acquire A
+% 	acquire B
+% 		acquire C
+% 			//Do stuff
+% 		release C
+% 	release B
+% release A
+% \end{lstlisting}
+% \end{tabular}
+% \end{table}
+
+% Once internal scheduling is introduce however, semantics of \gls{group-acquire} become relevant. For example, let us look into the semantics of the following pseudo-code :
+
+% \begin{lstlisting}[language=Pseudo]
+% 1: monitor A, B, C
+% 2: condition c1
+% 3: 
+% 4: acquire A
+% 5: 		acquire A & B & C
+% 6: 				signal c1
+% 7: 		release A & B & C
+% 8: release A
+% \end{lstlisting}
+
+% Without \gls{group-acquire} signal simply baton passes the monitor lock on the next release. In the case above, we therefore need to indentify the next release. If line 8 is picked at the release point, then the signal will attempt to pass A \& B \& C, without having ownership of B \& C. Since this violates mutual exclusion, we conclude that line 7 is the only valid location where signalling can occur. The traditionnal meaning of signalling is to transfer ownership of the monitor(s) and immediately schedule the longest waiting task. However, in the discussed case, the signalling thread expects to maintain ownership of monitor A. This can be expressed in two differents ways : 1) the thread transfers ownership of all locks and reacquires A when it gets schedulled again or 2) it transfers ownership of all three monitors and then expects the ownership of A to be transferred back. 
+
+% However, the question is does these behavior motivate supporting acquireing non-disjoint set of monitors. Indeed, if the previous example was modified to only acquire B \& C at line 5 (an release the accordingly) then in respects to scheduling, we could add the simplifying constraint that all monitors in a bulk will behave the same way, simplifying the problem back to a single monitor problem which has already been solved. For this constraint to be acceptble however, we need to demonstrate that in does not prevent any meaningful possibilities. And, indeed, we can look at the two previous interpretation of the above pseudo-code and conclude that supporting the acquiring of non-disjoint set of monitors does not add any expressiveness to the language.
+
+% Option 1 reacquires the lock after the signal statement, this can be rewritten as follows without the need for non-disjoint sets :
+% \begin{lstlisting}[language=Pseudo]
+% monitor A, B, C
+% condition c1
+
+% acquire A & B & C
+% 	signal c1
+% release A & B & C
+% acquire A
+
+% release A
+% \end{lstlisting}
+
+% This pseudo code has almost exaclty the same semantics as the code acquiring intersecting sets of monitors. 
+
+% Option 2 uses two-way lock ownership transferring instead of reacquiring monitor A. Two-way monitor ownership transfer is normally done using signalBlock semantics, which immedietely transfers ownership of a monitor before getting the ownership back when the other thread no longer needs the monitor. While the example pseudo-code for Option 2 seems toe transfer ownership of A, B and C and only getting A back, this is not a requirement. Getting back all 3 monitors and releasing B and C differs only in performance. For this reason, the second option could arguably be rewritten as : 
+
+% \begin{lstlisting}[language=Pseudo]
+% monitor A, B, C
+% condition c1
+
+% acquire A
+% 	acquire B & C
+% 		signalBlock c1
+% 	release B & C
+% release A
+% \end{lstlisting}
+
+% Obviously, the difference between these two snippets of pseudo code is that the first one transfers ownership of A, B and C while the second one only transfers ownership of B and C. However, this limitation can be removed by allowing user to release extra monitors when using internal scheduling, referred to as extended internal scheduling (pattent pending) from this point on. Extended internal scheduling means the two following pseudo-codes are functionnaly equivalent : 
+% \begin{table}[h!]
+% \centering
+% \begin{tabular}{c @{\hskip 0.65in} c}
+% \begin{lstlisting}[language=pseudo]
+% monitor A, B, C
+% condition c1
+
+% acquire A
+% 	acquire B & C
+% 		signalBlock c1 with A
+% 	release B & C
+% release A
+% \end{lstlisting} &\begin{lstlisting}[language=pseudo]
+% monitor A, B, C
+% condition c1
+
+% acquire A
+% 	acquire A & B & C
+% 		signal c1
+% 	release A & B & C
+% release A
+% \end{lstlisting}
+% \end{tabular}
+% \end{table}
+
+% It must be stated that the extended internal scheduling only makes sense when using wait and signalBlock, since they need to prevent barging, which cannot be done in the context of signal since the ownership transfer is strictly one-directionnal. 
+
+% One critic that could arise is that extended internal schedulling is not composable since signalBlock must be explicitly aware of which context it is in. However, this argument is not relevant since acquire A, B and C in a context where a subset of them is already acquired cannot be achieved without spurriously releasing some locks or having an oracle aware of all monitors. Therefore, composability of internal scheduling is no more an issue than composability of monitors in general.
+
+% The main benefit of using extended internal scheduling is that it offers the same expressiveness as intersecting monitor set acquiring but greatly simplifies the selection of a leader (or representative) for a group of monitor. Indeed, when using intersecting sets, it is not obvious which set intersects with other sets which means finding a leader representing only the smallest scope is a hard problem. Where as when using disjoint sets, any monitor that would be intersecting must be specified in the extended set, the leader can be chosen as any monitor in the primary set.
 
 % We need to make sure the semantics for internally scheduling N monitors are a natural extension of the single monitor semantics. For this reason, we introduce the concept of \gls{mon-ctx}. In terms of context internal scheduling means "releasing a \gls{mon-ctx} and waiting for an other thread to acquire the same \gls{mon-ctx} and baton-pass it back to the initial thread". This definitions requires looking into what a \gls{mon-ctx} is and what the semantics of waiting and baton-passing are.
Index: doc/proposals/concurrency/style.tex
===================================================================
--- doc/proposals/concurrency/style.tex	(revision 03bb816f896612125c8f1acd78ef46603e99f236)
+++ doc/proposals/concurrency/style.tex	(revision ffc9f5a7c031fc9030b12c8b0ca2d84dc9cd6d78)
@@ -1,5 +1,5 @@
 \input{common}                                          % bespoke macros used in the document
 
-\CFADefaultStyle
+% \CFADefaultStyle
 
 \lstset{
Index: doc/proposals/concurrency/version
===================================================================
--- doc/proposals/concurrency/version	(revision 03bb816f896612125c8f1acd78ef46603e99f236)
+++ doc/proposals/concurrency/version	(revision ffc9f5a7c031fc9030b12c8b0ca2d84dc9cd6d78)
@@ -1,1 +1,1 @@
-0.7.134
+0.7.141