VCC

Dość szczegółowe omówienie działania VCC można znaleźć w tym dokumencie:

http://research.microsoft.com/en-us/um/people/moskal/pdf/vcc-tutorial-2col.pdf

Dłuższa notatka na temat samego mechanizmu od współbieżności:

http://research.microsoft.com/en-us/um/people/moskal/pdf/local.pdf

Główne cechy wspomnainego mechanizmu to:

• Każdy obiekt ma właściciela (może się zmieniać w czasie -- w zasadzie to prostu pole 'ghost').
• Żeby rozpakować obiekt (tz. uzyskać prawo do zmieniania go i naruszania jego niezmienników), trzeba uczynić bieżący wątek jego właścicielem.
• Własność niekiedy traktowana jest przechodnio, co ma chyba dawać mechanizm podobny do grup danych w JML.
• Nie do końca jeszcze rozumiem pojęcie 'claims'. Jest to jakiś rodzaj referencji, dzięki którym jeden wątek może zapewnić, że obiekt należący do innego w¹tku pozostanie spójny.
• Dwustanowe niezmienniki mówią, jak może się zmienić obiekt w wyniku atomowej operacji. Konkretnie są opisane tu:

http://research.microsoft.com/pubs/118664/VCClocal.pdf

Concurrent Spec#

Metody stosowane w współbieżnych waeriantach Spec# są chyba pdobne do tych opisanych wyżej. Dośc pobieżne omówienie można znaleźc tu:

https://research.microsoft.com/en-us/projects/specsharp/concurrency.pdf

Chalice

Chalice to język do modelowania współbieżności, który tłumaczony jest do Boogie. Jego działanie (w tym proces translacji) jest opisane tu:

http://research.microsoft.com/en-us/um/people/leino/papers/krml191.pdf

Inny dokument, skupiający się raczej na zastosowaniu Chalice niż na implementacji:

http://research.microsoft.com/en-us/um/people/leino/papers/krml197.pdf