@@ -642,6 +642,7 @@ The keywords are:
642
642
@tab @code {syntax }
643
643
@tab @code {mutable }
644
644
@tab @code {native }
645
+ @tab @code {unchecked }
645
646
@item @code {mod }
646
647
@tab @code {import }
647
648
@tab @code {export }
@@ -679,7 +680,7 @@ The keywords are:
679
680
@tab @code {with }
680
681
@item @code {fn }
681
682
@tab @code {iter }
682
- @tab @code {pred }
683
+ @tab @code {pure }
683
684
@tab @code {obj }
684
685
@tab @code {resource }
685
686
@item @code {if }
@@ -1252,15 +1253,6 @@ immediately destructed (if acyclic) or else collected using a general
1252
1253
(cycle-aware) garbage-collector local to each task. Garbage collection within
1253
1254
a local heap does not interrupt execution of other tasks.
1254
1255
1255
- Immutable boxes are @dfn {shared }, and can be multiply-referenced by many
1256
- different tasks. Like any other immutable type, they can pass over channels,
1257
- and live as long as the last task referencing them within a given domain. When
1258
- unreferenced, they are destroyed immediately (due to reference-counting) and
1259
- returned to the heap memory allocator. Destruction of an immutable box also
1260
- executes within the context of the task that drops the last reference to a
1261
- shared heap allocation, so executing a long-running destructor does not
1262
- interrupt execution of other tasks.
1263
-
1264
1256
1265
1257
@node Ref.Mem.Own
1266
1258
@subsection Ref.Mem.Own
@@ -1396,25 +1388,23 @@ fn main() @{
1396
1388
@node Ref.Mem.Acct
1397
1389
@subsection Ref.Mem.Acct
1398
1390
@c * Ref.Mem.Acct:: Memory accounting model.
1399
- @cindex Domain
1400
1391
@cindex Accounting
1401
1392
@cindex Memory budget
1402
1393
1403
- Every task belongs to a domain, and that domain tracks the amount of memory
1404
- allocated and not yet released by tasks within it. @xref {Ref.Task.Dom }. Each
1405
- domain has a memory budget. The @dfn {budget } of a domain is the maximum amount
1406
- of memory that can be simultaneously allocated in the domain. If a task tries
1407
- to allocate memory within a domain with an exceeded budget, the task will
1408
- receive a signal.
1394
+ Every task tracks the amount of memory allocated and not yet released. Each
1395
+ task may have a memory budget. The @dfn {budget } of a task is the maximum
1396
+ amount of memory that can be simultaneously allocated in the task. If a task
1397
+ tries to allocate memory with an exceeded budget, the task will receive a
1398
+ signal.
1409
1399
1410
1400
Within a task, accounting is strictly enforced: all memory allocated through
1411
- the runtime library, both user data, sub-domains and runtime-support
1412
- structures such as channel and signal queues, are charged to a task's domain .
1401
+ the runtime library, both user data and runtime-support structures such as
1402
+ channel and signal queues, are charged to a task.
1413
1403
1414
- When a communication channel crosses from one domain to another, any value
1404
+ When a communication channel crosses from one task to another, any value
1415
1405
sent over the channel is guaranteed to have been @emph {detached } from the
1416
- domain 's memory graph (singly referenced, and/or deep-copied), so its memory
1417
- cost is transferred to the receiving domain .
1406
+ task 's memory graph (singly referenced, and/or deep-copied), so its memory
1407
+ cost is transferred to the receiving task .
1418
1408
1419
1409
1420
1410
@page
@@ -1439,7 +1429,6 @@ operating-system processes.
1439
1429
@menu
1440
1430
* Ref.Task.Comm :: Inter-task communication.
1441
1431
* Ref.Task.Life :: Task lifecycle and state transitions.
1442
- * Ref.Task.Dom :: Task domains.
1443
1432
* Ref.Task.Sched :: Task scheduling model.
1444
1433
* Ref.Task.Spawn :: Library interface for making new tasks.
1445
1434
* Ref.Task.Send :: Library interface for sending messages.
@@ -1492,12 +1481,12 @@ transmit side. A channel contains a message queue and asynchronously sending a
1492
1481
message merely inserts it into the sending channel's queue; message receipt is
1493
1482
the responsibility of the receiving task.
1494
1483
1495
- Queued messages in channels are charged to the domain of the @emph {sending }
1496
- task. If too many messages are queued for transmission from a single sending
1497
- task, without being received by a receiving task, the sending task may exceed
1498
- its memory budget, which causes a run-time signal. To help control this
1499
- possibility, a semi-synchronous send operation is possible, which blocks until
1500
- there is room in the existing queue before sending send.
1484
+ Queued messages in channels are charged to the @emph {sending } task. If too
1485
+ many messages are queued for transmission from a single sending task, without
1486
+ being received by a receiving task, the sending task may exceed its memory
1487
+ budget, which causes a run-time signal. To help control this possibility, a
1488
+ semi-synchronous send operation is possible, which blocks until there is room
1489
+ in the existing queue before sending send.
1501
1490
1502
1491
Messages are sent on channels and received on ports using standard library
1503
1492
functions.
@@ -1560,31 +1549,6 @@ A task in the @emph{dead} state cannot transition to other states; it exists
1560
1549
only to have its termination status inspected by other tasks, and/or to await
1561
1550
reclamation when the last reference to it drops.
1562
1551
1563
- @node Ref.Task.Dom
1564
- @subsection Ref.Task.Dom
1565
- @c * Ref.Task.Dom:: Task domains
1566
-
1567
- @cindex Domain
1568
- @cindex Process
1569
- @cindex Thread
1570
-
1571
- Every task belongs to a domain. A @dfn {domain } is a structure that owns tasks,
1572
- schedules tasks, tracks memory allocation within tasks and manages access to
1573
- runtime services on behalf of tasks.
1574
-
1575
- Typically each domain runs on a separate operating-system @emph {thread }, or
1576
- within an isolated operating-system @emph {process }. An easy way to think of a
1577
- domain is as an abstraction over either an operating-system thread @emph {or } a
1578
- process.
1579
-
1580
- The key feature of a domain is that it isolates memory references created by
1581
- the Rust tasks within it. No Rust task can refer directly to memory outside
1582
- its domain.
1583
-
1584
- Tasks can own sub-domains, which in turn own their own tasks. Every domain
1585
- owns one @emph {root task }, which is the root of the tree of tasks owned by the
1586
- domain.
1587
-
1588
1552
@node Ref.Task.Sched
1589
1553
@subsection Ref.Task.Sched
1590
1554
@c * Ref.Task.Sched:: Task scheduling model.
@@ -1593,11 +1557,9 @@ domain.
1593
1557
@cindex Preemption
1594
1558
@cindex Yielding control
1595
1559
1596
- Every task is @emph {scheduled } within its domain. @xref {Ref.Task.Dom }. The
1597
- currently scheduled task is given a finite @emph {time slice } in which to
1560
+ The currently scheduled task is given a finite @emph {time slice } in which to
1598
1561
execute, after which it is @emph {descheduled } at a loop-edge or similar
1599
- preemption point, and another task within the domain is scheduled,
1600
- pseudo-randomly.
1562
+ preemption point, and another task within is scheduled, pseudo-randomly.
1601
1563
1602
1564
An executing task can @code {yield } control at any time, which deschedules it
1603
1565
immediately. Entering any other non-executing state (blocked, dead) similarly
@@ -1616,7 +1578,7 @@ function. The passed function is referred to as the @dfn{entry function} for
1616
1578
the spawned task, and any captured environment is carries is moved from the
1617
1579
spawning task to the spawned task before the spawned task begins execution.
1618
1580
1619
- The result of a @code {spawn } call is a @code {std::task::task_id } value.
1581
+ The result of a @code {spawn } call is a @code {std::task::task } value.
1620
1582
1621
1583
An example of a @code {spawn } call:
1622
1584
@example
@@ -1631,10 +1593,10 @@ fn helper(c: chan<u8>) @{
1631
1593
1632
1594
let p: port<u8>;
1633
1595
1634
- spawn(bind helper(p.mk_chan( )));
1596
+ spawn(bind helper(chan(p )));
1635
1597
// let task run, do other things.
1636
1598
// ...
1637
- let result = p. recv();
1599
+ let result = recv(p );
1638
1600
1639
1601
@end example
1640
1602
@@ -1674,7 +1636,7 @@ An example of a @emph{receive}:
1674
1636
@example
1675
1637
import std::comm::*;
1676
1638
let p: port<str> = @dots {};
1677
- let s: str = p. recv();
1639
+ let s: str = recv(p );
1678
1640
@end example
1679
1641
1680
1642
@@ -1931,7 +1893,7 @@ control).
1931
1893
Any pure boolean function is called a @emph {predicate }, and may be used
1932
1894
as part of the static typestate system. @xref {Ref.Typestate.Constr }. A
1933
1895
predicate declaration is identical to a function declaration, except that it
1934
- is declared with the keyword @code {pred } instead of @code { fn }. In addition,
1896
+ is declared with the additional keyword @code {pure }. In addition,
1935
1897
the typechecker checks the body of a predicate with a restricted set of
1936
1898
typechecking rules. A predicate
1937
1899
@itemize
@@ -1942,11 +1904,65 @@ self-call expression; and
1942
1904
1943
1905
An example of a predicate:
1944
1906
@example
1945
- pred lt_42(int x ) -> bool @{
1907
+ pure fn lt_42(x: int ) -> bool @{
1946
1908
ret (x < 42);
1947
1909
@}
1948
1910
@end example
1949
1911
1912
+ A non-boolean function may also be declared with @code {pure fn }. This allows
1913
+ predicates to call non-boolean functions as long as they are pure. For example:
1914
+ @example
1915
+ pure fn pure_length<@@ T>(ls: &list<T>) -> uint @{ /* ... */ @}
1916
+
1917
+ pure fn nonempty_list<@@ T>(ls: &list<T>) -> bool @{ pure_length(ls) > 0u @}
1918
+ @end example
1919
+
1920
+ In this example, @code {nonempty_list } is a predicate--- it can be used in a
1921
+ typestate constraint--- but the auxiliary function @code {pure_length }@ is
1922
+ not.
1923
+
1924
+ @emph {ToDo: } should actually define referential transparency.
1925
+
1926
+ The effect checking rules previously enumerated are a restricted set of
1927
+ typechecking rules meant to approximate the universe of observably
1928
+ referentially transparent Rust procedures conservatively. Sometimes, these
1929
+ rules are @emph {too } restrictive. Rust allows programmers to violate these
1930
+ rules by writing predicates that the compiler cannot prove to be referentially
1931
+ transparent, using an escape-hatch feature called ``unchecked blocks''. When
1932
+ writing code that uses unchecked blocks, programmers should always be aware
1933
+ that they have an obligation to show that the code @emph {behaves } referentially
1934
+ transparently at all times, even if the compiler cannot @emph {prove }
1935
+ automatically that the code is referentially transparent. In the presence of
1936
+ unchecked blocks, the compiler provides no static guarantee that the code will
1937
+ behave as expected at runtime. Rather, the programmer has an independent
1938
+ obligation to verify the semantics of the predicates they write.
1939
+
1940
+ @emph {ToDo: } last two sentences are vague.
1941
+
1942
+ An example of a predicate that uses an unchecked block:
1943
+ @example
1944
+ fn pure_foldl<@@ T, @@ U>(ls: &list<T>, u: &U, f: &block(&T, &U) -> U) -> U @{
1945
+ alt ls @{
1946
+ nil. @{ u @}
1947
+ cons(hd, tl) @{ f(hd, pure_foldl(*tl, f(hd, u), f)) @}
1948
+ @}
1949
+ @}
1950
+
1951
+ pure fn pure_length<@@ T>(ls: &list<T>) -> uint @{
1952
+ fn count<T>(_t: &T, u: &uint) -> uint @{ u + 1u @}
1953
+ unchecked @{
1954
+ pure_foldl(ls, 0u, count)
1955
+ @}
1956
+ @}
1957
+ @end example
1958
+
1959
+ Despite its name, @code {pure_foldl } is a @code {fn }, not a @code {pure fn },
1960
+ because there is no way in Rust to specify that the higher-order function
1961
+ argument @code {f } is a pure function. So, to use @code {foldl } in a pure list
1962
+ length function that a predicate could then use, we must use an
1963
+ @code {unchecked } block wrapped around the call to @code {pure_foldl } in the
1964
+ definition of @code {pure_length }.
1965
+
1950
1966
@node Ref.Item.Iter
1951
1967
@subsection Ref.Item.Iter
1952
1968
@c * Ref.Item.Iter:: Items defining iterators.
@@ -2748,7 +2764,7 @@ A @dfn{constraint} is a predicate applied to specific slots.
2748
2764
For example, consider the following code:
2749
2765
2750
2766
@example
2751
- pred is_less_than(int a, int b) -> bool @{
2767
+ pure fn is_less_than(int a, int b) -> bool @{
2752
2768
ret a < b;
2753
2769
@}
2754
2770
@@ -3525,7 +3541,7 @@ and statically comparing implied states and their
3525
3541
specifications. @xref {Ref.Typestate }.
3526
3542
3527
3543
@example
3528
- pred even(x: &int) -> bool @{
3544
+ pure fn even(x: &int) -> bool @{
3529
3545
ret x & 1 == 0;
3530
3546
@}
3531
3547
@@ -3724,7 +3740,7 @@ signal queue associated with each task. Sending a signal to a task inserts the
3724
3740
signal into the task's signal queue and marks the task as having a pending
3725
3741
signal. At the next scheduling opportunity, the runtime processes signals in
3726
3742
the task's queue using its dispatch table. The signal queue memory is charged
3727
- to the task's domain ; if the queue grows too big, the task will fail.
3743
+ to the task; if the queue grows too big, the task will fail.
3728
3744
3729
3745
@c ############################################################
3730
3746
@c end main body of nodes
0 commit comments