云鉴权>> transactional-futures-redex>> 返回
项目作者： jswalens

项目描述 ：
Executable semantics of transactional futures in PLT Redex.
高级语言： Racket
项目地址: git://github.com/jswalens/transactional-futures-redex.git
创建时间： 2016-04-28T12:52:57Z
项目社区：https://github.com/jswalens/transactional-futures-redex
开源协议：
下载


PLT Redex implementation of ClojureTxTk

This repository contains a machine-executable implementation of the operational semantics of ClojureTxTk, using PLT Redex.

It consists of the following files:

  • clj-base.rkt defines Lb, the “base” language (based on Clojure)
  • clj-futures.rkt defines Lf, the base language extended with support for futures (as in Clojure)
  • clj-tx.rkt defines Lt, which is Lf extended with support for transactions (as in Clojure)
  • tx-futs.rkt defines Ltf, which is Lt extended with support for transactional futures (not in Clojure)
  • map.rkt: helper functions for maps
  • set.rkt: helper functions for sets

Each of the files also contains test cases.

For instance, tx-futs.rkt contains the following test case (named example-tx-futs-3):

  1. (let [(r_0 (ref 0))
  2.       (f_0 (fork
  3.              (atomic
  4.                (let [(x (fork (ref-set r_0 (+ (deref r_0) 1))))
  5.                      (y (fork (ref-set r_0 (+ (deref r_0) 2))))]
  6.                  (do (join x) ; => r_0 = original + 1
  7.                    (join y)   ; => r_0 = original + 2
  8.                    (deref r_0)))))) ; => returns original + 2
  9.        (f_1 (fork
  10.               (atomic
  11.                 (let [(x (fork (ref-set r_0 (+ (deref r_0) 3))))
  12.                       (y (fork (ref-set r_0 (+ (deref r_0) 4))))]
  13.                   (do (join x) ; => r_0 = original + 3
  14.                     (join y)   ; => r_0 = original + 4
  15.                     (deref r_0))))))] ; => returns original + 4
  16.   (+ (join f_0) (join f_1)))

There are two possible outcomes of this program:

  1. (term [[(f_0 8) (f_new1 6) (f_new 2)]
  2.        [(r_new 6) (r_new 5) (r_new 2) (r_new 1) (r_new 0)]])
  3. (term [[(f_0 10) (f_new1 4) (f_new 6)]
  4.        [(r_new 6) (r_new 5) (r_new 4) (r_new 3) (r_new 0)]])

These correspond to the two possible serializations: the first corresponds to transaction 1 executing first (end result is 8), the second to transaction 2 executing first (end result is 10).

These results can be visualized using:

  1. (traces ->tf example-tx-futs-3)

This is shown in the image in example-tx-futs-3.pdf. You can see how different interleavings lead to different intermediate states, but they collapse into two final states, corresponding to the two possible serializations.