kaist-cp / cs431 Goto Github PK

On Wednesday, September 11th, the professor did not take attendance for the Concurrent programmng course, but I did attend the class. Now, when I log into my attendance portal, I see a "No" for that Wednesday's class. I was wondering if you could please correct it, because I was indeed present in class.

I have a question about the reasonable performance of ART (CS492 homework#1).

In the stress test, it performs 4096 * 4096 operations to ART.

And when I tested my ART,

(Tested environment: Processor: 1.1GHz *2; Memory: 1867 MHz LPDDR3)

Is it fast enough, or does it need to be more optimized?

In the lecture slide p30, relaxed behaviors is observable behaviors not captured in the interleaving semantics.
Then, what is interleaving semantics?

The reason I asked this is I understand in the class that relaxed behaviors happens when there is reordering and non-determinism, but when I looking at the definition above, I cannot quite get the concept of relaxed behaviors.

To make a short story short: Could you explain what is interleaving semantics?

• Also, out of thin air(OOTA) is the situation that the desired output cannot be reached in the context?

I'm wondering how I prove a given program is a correct lock. Informally, I believe that a lock must provide two main features:

1. Mutual exclusion: if thread A is holding a lock L, other threads cannot hold L.
2. Acquire-release of thread-wise views: whenever thread A unlocks L, view of A is released to L; another thread to hold L acquires its view.

However I'm still curious about writing proper proof in (1) midterm exam and (2) formal reasoning. How can I do?

While implementing ART I ran into several cases where I had to use unsafe codes like raw ptr deref, std::ptr:: functions, and

unsafe { &mut *(v as &_ as *const _ as *mut _ as &mut T) ... }

Now I'm getting use-after-free errors so I decided to clean things up. But I'm still not sure how much unsafety we need in this HW.

What is the precise meaning of relaxed behaviors and relaxed orderings?

It is written "Guaranteeing fairness by ordering & waiting w/ different locations"(slide 70). However, I thought that fairness is achieved only by ordering. Could you, please, explain how fairness is achieved by waiting w/ different locations? Thank you!

T1:
r2 = Y
fence(SC)
X = 1

T2:
r1 = X
Y = r1

// r1 = r2 = 1  allowed?

I tried:

1. Suppose I promise and certify X = 1@1 at T1.
2. I execute T2 sequentially.
3. I execute T1 to re-certify X = 1. At that moment, r2 becomes 1 read from Y and move the global view { X: 0@0, Y: 0@0 } to { X: 0@0, Y: 1@2} since T1's view is also { X: 0@0, Y: 1@2}.
4. Finally, I can re-certify X = 1@1 and judge this behavior is allowed.

Question

However, It's weird because, as I know, it cannot be reordered by store-hoisting due to fence(SC) which forbids to reorder the program order back and forth. But it seems to be allowed on Promising Semantics. Did I miss something?

Hi.
I didn't get the concept of the cursor.
Can you show how the cursor struct will be where the cursor is placed in the purple line?

Is it okay to represent like below?
Cursor {
depth : 1,
parent : red node,
child : blue node,
index : 1,
length : 2,
}

Thank you.

This is impl of NodeBody256's lookup method.

impl<V> NodeBodyI<V> for NodeBody256<V> {
    fn lookup(&self, key: u8) -> Option<(u8, &NodeBox<V>)> {
        Some((key, unsafe {
            self.children.get_unchecked(usize::from(key))
        }))
    }
}

I think this lookup function should return None when there's no child.
But it returns always Some. Is this expected behavior?

Dear Professor,

I was not able to log into gg.kaist.ac.kr. I don't know how you manage it and whether you manually manage each student's access to the website, but could you please check it and tell me what could we do to solve the problem?

Have other students successfully entered the website?

I think I cannot get a concept of cursor right now. So I have hard time to understand the role of cursor method. Obviously, this method returns Cursor struct with given key.

1. In initial state, i.e. there's only root node. What will be return value of cursor method with key "FOO"?

After call insert("FOO",VAL), I expect that state of ART struct will be changed as above. (Am I right? If there's something wrong, please tell me.) Then Cursor returned by input "FOO" will be

{
depth : 1
parent: root
child: leaf node
index: 0
length: (I cannot understand this part)
}

Is it right? And can you explain me again about the role of length?

3. In above state, what will be returned if we call cursor method with key "FOL"?

+) I didn't read every code line by line, but it seems that almost every part is implemented and the part we have to implement is just "cursor" method of ART, and "or_insert_with", "delete" method of Entry. Right?

++) It's general Rust question. I expect that next() in main function return 1 and 2. But it returns 3 and none. What do I have to do if I want to refresh the iterator?

fn foo1<T: std::iter::Iterator>(v : &mut T)
{
    v.next();
    v.next();
}

fn main() 
{
    let mut v= [1,2,3];
    let mut vt=v.iter();
    foo1(&mut vt);
    println!("{}", vt.next().unwrap());
    println!("{}", vt.next().unwrap());
}

From slide 30:

"Assertion failure due to reordering in the left thread or in the right thread"
In the case of the left thread reordering, I can see why assertion fails(1)FLAG.store(1); 2)right thread 3)DATA = 42;). However, I cannot imagine how the right thread should be reordered in order for the assertion to fail?

Thank you!

I have a few of questions about Peterson's mutex.

static flag: [AtomicBool; 2];
static turn: AtomicUsize;

fn begin(id: usize) {
    flag[id].store(true);
    fence(SeqCst);    // A
    turn.store(1 - id);
    fence(SeqCst);    // B

    while flag[1 - id].load(acquire) && turn.load() == 1 - id {}    
}

fn end(id: usize) {
    flag[id].store(false, release);
}

1. Some ordering of operations are omitted. Are all of them relaxed?

2. If so, why turn should be atomic? Just for avoiding unsafe?

3. What does make compiler not to optimize turn.load() == 1 - id into true? I suspect that readonly reference to turn, which has interior mutability makes reading turn be volatile. If so, suppose this code is rewritten in C. Then do I need to denote turn by volatile?

4. I conject that fence B ensures turn.load() to read the latest message of turn. But I think this is unnecessary, since turn.store(1 - id) cannot be reordered after turn.load(). Looking at spinlock, it does not ensures compare-and-swap reads the latest flag. Is there another reason for fence B?

From the slide 15: "Exclusive: resource is read/written by its designated owner...". Could you, please, give a code example when resource is written by owner? I tried to come up with one, but couldn't.
fn main() { let mut s = String::from("hello"); s.push('w'); }
For example here, the modification( s.push) is done by exclusive borrowing, and not the owner s itself. So, I am confused, how s - the owner can make modifications, even if its own methods do modifications by borrowing.

Thank you!

From the slide 18:
"List up the pairs of overlapping lifetimes
“v” and “p” (L3-L5), “v” and “v.push” (L4)
“p” and “v.push” (L4)

Ignore borrowed & borrowing ones
“p” and “v.push” (L4) remained"

What does "Ignore borrowed & borrowing ones" mean? In the example provided, it seems like we are ignoring "owner and borrower" pairs, and leaving "borrower and borrower" pairs instead.

Also, it seems like code needs to be updated: let v = vec![1, 2, 3]; -> let mut v = vec![1, 2, 3];
`fn main() {
let v = vec![1, 2, 3];

let p = &v[1];
v.push(4);
println!("v[1]: {}", *p);

}`
Thank you!

Causality test case 12

Initially, x = y = 0; a[0] = 1, a[1] = 2

Thread 1
r1 = x
a[r1] = 0
r2 = a[0]
y = r2

Thread 2
r3 = y
x = r3

Behavior in question: r1 = r2 = r3 = 1

Decision: Disallowed. Since no other thread accesses the array a,
the code for thread 1 should be equivalent to

r1 = x
a[r1] = 0
if (r1 == 0)
      r2 = 0
    else
      r2 = 1
y = r2


With this code, it is clear that this is the same situation as
test 4.

In the answer, it's written that behavior is disallowed. However, it seems that there is the case when r1 = r2 = r3 = 1 can happen(described bellow). Am I missing something?

`Thread 1
r2 = a[0]
y = r2
r1 = x
a[r1] = 0

Thread 2
r3 = y
x = r3

Scheduling goes as following:
Thread 1
r2 = a[0]
y = r2
Thread 2
r3 = y
x = r3
Thread 1
r1 = x
a[r1] = 0

In this way r1 = r2 = r3 = 1
`

Thank you!

It seems thatnew_path in node.rs assumes nodes are structured like below:

key is 1, 2, 3, 4, 5, 6 ,7, 8 ....

//    +--------------------------------+ (root)
//    |Node Box Intermediate 4         |
//    |                                |
//    |  +--------------------------+  |
//    |  |Node Header               |  |
//    |  | length: u8               |  |
//    |  | key   : [1, 2, 3, 4,   ] |  |
//    |  +--------------------------+  |
//    |  +--------------------------+  |
//    |  |Node Body 4               |  |
//    |  | keys    : [5][ ][ ][ ]   |  | // -------------------------(1)
//    |  | children: [+][ ][ ][ ]   |  |
//    |  +--------------------------+  |
//    +--------------------------------+
//                    |
//    v---------------+
//    +--------------------------------+ (child)
//    |Node Box Intermediate 4         |
//    |                                |
//    |  +--------------------------+  |
//    |  |Node Header               |  |
//    |  | length: u8               |  |
//    |  | key   : [5, 6, 7, 8,...] |  | // -------------------------(2)
//    |  +--------------------------+  |
//    |  +--------------------------+  |
//    |  |Node Body 4               |  |
//    |  | keys    : [x][ ][ ][ ]   |  |
//    |  | children: [+][ ][ ][ ]   |  |
//    |  +--------------------------+  |
//    +--------------------------------+
//                    |
//                    |
//    v---------------+
//    +--------------------------------+
//    |Node Box Leaf                   |
//    |                                |
//    |  +--------------------------+  |
//    |  |Node Header               |  |
//    |  | length: u8               |  |
//    |  | key   : [remain keys...] |  |
//    |  +--------------------------+  |
//    |  +--------------------------+  |
//    |  |Node Body V               |  |
//    |  |                          |  |
//    |  |                          |  |
//    |  +--------------------------+  |
//    +--------------------------------+

The key element '5' in (1) and (2) is saved repeatedly. (I've also checked via debugging)

However, algorithm in Figure 7 in the paper fails to search.

Fig 7. Search algorithm

search (node, key, depth) //----- (1)
    if node==NULL
        return NULL
    if isLeaf(node)
        if leafMatches(node, key, depth)
            return node
        return NULL
    if checkPrefix(node,key,depth)!=node.prefixLen // ------- (2)
        return NULL
    depth=depth+node.prefixLen // ------- (3)
    next=findChild(node, key[depth]) // --------- (4)
    return search(next, key, depth+1) // ---------- (5)

Steps:

-- First call
(1) search (root, key, 0)
(2) checkPrefix(root, key, 0) == 4 == root.prefixLen
(2-1) key[0] == prefix[0] == 1
(3) depth is now 4
(4) key[4] is 5, child = findChild(root, 5)
(5) search(child, key, 5)// 5 = depth + 1

-- Second call
(1) search (child, key, 5)
(2) checkPrefix(root, key, 5) will fail because key[5] ( is 6) != prefix[0] ( is 5)

I think the algorithm expect a structure like below:

//    +--------------------------------+ (root)
//    |Node Box Intermediate 4         |
//    |                                |
//    |  +--------------------------+  |
//    |  |Node Header               |  |
//    |  | length: u8               |  |
//    |  | key   : [1, 2, 3, 4,   ] |  |
//    |  +--------------------------+  |
//    |  +--------------------------+  |
//    |  |Node Body 4               |  |
//    |  | keys    : [5][ ][ ][ ]   |  | // -------------------------(1)
//    |  | children: [+][ ][ ][ ]   |  |
//    |  +--------------------------+  |
//    +--------------------------------+
//                    |
//    v---------------+
//    +--------------------------------+ (child)
//    |Node Box Intermediate 4         |
//    |                                |
//    |  +--------------------------+  |
//    |  |Node Header               |  |
//    |  | length: u8               |  |
//    |  | key   : [6, 7, 8, 9,...] |  | // -------------------------(2)
//    |  +--------------------------+  |
//    |  +--------------------------+  |
//    |  |Node Body 4               |  |
//    |  | keys    : [x][ ][ ][ ]   |  |
//    |  | children: [+][ ][ ][ ]   |  |
//    |  +--------------------------+  |
//    +--------------------------------+
//                    |
//                    |
//    v---------------+
//    +--------------------------------+
//    |Node Box Leaf                   |
//    |                                |
//    |  +--------------------------+  |
//    |  |Node Header               |  |
//    |  | length: u8               |  |
//    |  | key   : [remain keys...] |  |
//    |  +--------------------------+  |
//    |  +--------------------------+  |
//    |  |Node Body V               |  |
//    |  |                          |  |
//    |  |                          |  |
//    |  +--------------------------+  |
//    +--------------------------------+

Which structure should I follow?

This is Causality test case 11

Initially, x = y = z = 0

Thread 1:
r1 = z
w = r1
r2 = x
y = r2

Thread 2:
r4 = w
r3 = y
z = r3
x = 1

x=1 can be certified in T2. But how can I certify y=1?
I'm confused because T1 has no assignment, so it cannot certify anything alone.

Hi.

I am wondering that why the lookup function for the NodeBodyI returns the input key.

I think returning the reference to the node is enough because the caller knows the key already.

Can you explain please?

Thank you.

While configure CodeLLDB in launch.json in VSCode(Mac OSX),
what is the proper path for program?
I configured art/target/debug/deps/art_test-HASH, but it does not work. (Process exited with code 101.)
Does of you succeed to configure CodeLLDB on VSCode, can you give me some help?

Could you, please, show how promising semantics allows r1 = r2 = r3 = 1 behavior in causality test case 7? Where did I go wrong in my attempt?

My attempt:

1. initial state:
   

2. Thread 2 makes a promise to write 1 to X. It's certified, as t2 can write 1 to X by itself.
   

3. After the execution of thread 1: r1 = 0, r2 = 1
   

4. After the execution of thread 2: r3 = 1, the promised message is re-certified
   

So, I got in the end r1 = 0, r2 = r3 = 1

I also tried executing t2 first, and then t1. However, I get r1=r3=0, r2 = 1

For reference:
Causality test case 7

Initially, x = y = z = 0

Thread 1:
r1 = z
r2 = x
y = r2

Thread 2:
r3 = y
z = r3
x = 1

Behavior in question: r1 = r2 = r3 = 1.

Decision: Allowed. Intrathread transformations could move r1 = z to
after the last statement in thread 1, and x = 1 to before the
first statement in thread 2.

During testing my ART (based on the commit @20b07e2) with stress test with >30000 ops, I found that the behavior of the method extract_children of NodeBody48<V> is slightly different from the methods of other ones.

For example, suppose that NodeBody contains 4 key-value pairs, (7, a), (9, b), (8, c), (6, d).

Then, NodeBody4 and NodeBody16 can contain them such as key = [7, 9, 8, 6, ...], and children=[a, b, c, d, ...]. When we call extract_children with this node, the method will zip them using izip! and make a vector by pushing zipped one. Therefore, we obtain a vector [(7, a), (9, b), (8, c), (6, d)].

If NodeBody256 contains above 4 pairs, then children is an array such that children[7] = a, children[9] = b, children[8] = c and children[6] = d. When we call extract_children with this node, the method enumerates children by index and make a vector of index-value pairs. Therefore, we obtain a vector [(6, d), (7, a), (8, c), (9, d)].

If NodeBody48 contains above 4 pairs, then indexes may be an array such as children[7] = 0, children[9] = 1, children[8] = 2, children[6] = 3, and children may be an array [a, b, c, d, ...]. When we call extract_children with this node, the method iterates the values of indexes and make a vector of index-value pairs. But the index part of the vector is not the index of indexes but one of children. Therefore, we obtain a vector [(0, a), (1, b), (2, c), (3, d)].

I want to know whether I misunderstood the code (and this difference was intended).

If I insert "FOO", tree should have root node and leaf node only.

Then, I search "FO", Entry has

Cursor

• depth: 2
• parent: root
• child: leaf
• index: 0
• length: 2

Key: None

When lookup function evaluates, it should be failed.
Because child.header.length(3, "FOO") is not equal self.cursor.length(2, "FO")

What is wrong?

Thanks

• Helpdesk is here: https://github.com/kaist-cp/helpdesk/issues
• Technical questions of any kind are very much encouraged.
• Please watch the helpdesk repository. When a new question or answer is written, an email will be automatically delivered to you.

Hello,
I was wondering when the exact midterm date is.

I'll be absent on 9/4, so there will be no class in the classroom. Instead, I will upload a video explaining the course material. Instead, I will upload the slides so that you can study them on your own. You are required to study the slides before 9/9.

Now you can submit your token within 12 hours from the beginning of a session. See the following page for further details: https://github.com/kaist-cp/cs492-concur#attendance-

I have a question about causality test case 14.

Initially, a = b = y = 0, y is volatile

Thread 1:
r1 = a
if (r1 == 0)
y = 1
else
b = 1

Thread 2:
do {
r2 = y
r3 = b
} while (r2 + r3 == 0);
a = 1;

Behavior in question: r1 == r3 = 1; r2 = 0

Decision: Disallowed In all sequentially consistent executions, r1 = 0 and
the program is correctly synchronized. Since the program is correctly
synchronized in all SC executions, no non-sc behaviors are allowed.

1. Is it right the reason why a=1 cannot promise is that without thread 1, thread 2 will keep looping at do/while, so we cannot certify that a=1?

2. What is function of volatile?

Thanks.

1. by README.md, You don’t need to shrink a node even if it’s underfull.
   It means empty node(has no children) can be exist?

2. delete(...) returns Result<V, ()>. But I can get only &V (or &mut V)
   When I try to dereference it, cannot move error occurs.
   Can you give me a hint about solving this problem?

Hello, could you please comment on why the behavior in below slide is concluded to be disallowed?
In other words, what argument does promising semantics make, in order to reject re-certification of writing the promise, X=1?

I am confused on the concept of ownership and borrowing in the example presented on the screenshot below:

In this case, because function 'return_string' is borrowing the value, it doesn't give the ownership of value from s1 to s2, so this means that it passes the reference to s2(as far as I understood).
So, smth like this happens:

However, this kind of behaviour should not be allowed in Rust, because there can be only one owner of variable, in order to avoid double free bug.

Could you, please, explain, what is happening in that example, how is that possible(does it really make two variables to point to the same value, does it do deep copy or smth else)?

Thank you!

1. Does load(acquire) make it mandatory for the thread to load the message only with the per-message view annotated into it? In other words, in the example presented above, the dark green thread has to read Y=1 (it can't read Y=0), because Y=1 has per-message view annotated into it?
2. In case there are several threads executing store( , release), when executing one load(acquire) which of the store( , release) messages thread should read?

On slide 31, it's hard for me to distinguish between "store hoisting" and "load hoisting". As far as I understood, "load hoisting" allows loading older values from a variable. However, "store hoisting" also seems to do a similar thing - loading older values from a variable. What is "store hoisting" and how is it different from "load hoisting"?

Thank you!

Could you, please, explain, how do views behave with rmw instructions?
For example:

1. In order to avoid such situations, does this mean that if one of the threads wants to make rmw instruction on the variable, the thread should transfer its view to the latest rmw instruction's message(or just latest write message?) first, and only then perform rmw?
2. What happens in the case if some another thread(say t5) wants to read value from the variable which had rmw instructions performed on it? Should t5 read the message with timestamp >= the timestamp of latest rmw instruction's message made by other thread, or t5 can read the message with timestamp >= the timestamp of t5 current view's message?

I have an error of reasoning and I cannot get around what I am wrong about.
When trying to traverse the Tree I borrow the child to look up the key and cannot borrow the child again if I want to do the same thing for the next node. I also tried doing a helper function to do it recursively but the multiple returns end up producing multiple borrows as well.
Even disregarding that, trying to create an instance of Cursor with Information I get always leads to me needing to borrow the child.
I have a faulty approach but have run out of ideas and think that I have an error of approach.
Can you give me a hint for what I am doing fundamentally wrong?
(for what I understand: the cursor function is a function finding the edge at where the key should be/is)

Logistics

• Date & time: 9:00am-11:00am, October 21th, 2019
• Place: Rm. 2111, Bldg. E3-1
• Coverage: everything you’ve learned in this course
  • Including the code of locks and ART, and the ART paper
  • Not asking you to program in Rust in the paper
• Bring a black/blue pen and your student ID (no pencil, please)

Study guide

• You are asked to “explain” the reasons of a phenomena. Your explanation should be an informal proof with a few gaps. In other words, your argument should be clear and precise.

Read README.md for more details.

Causality test case 16

Initially, x = 0

Thread 1:
r1 = x
x = 1

Thread 2:
r2 = x
x = 2

Behavior in question: r1 == 2; r2 == 1

Decision: Allowed.

It is written on the lecture slides that case 16 is wrong. However, we can do load-store reordering in Thread 2, by doing this, r1 == 2; r2 == 1 will be allowed.

Execution:
Thread 2:
x = 2
Thread 1:
r1 = x
x = 1
Thread 2:
r2 = x

Am I missing something?
Thank you!

1. On slide 60, what is the difference between SpinLockand SpinLockGuard? Their second fields differ the most: SpinLock(data: UnsafeCell) and SpinLockGuard(_marker: PhantomData<*const ()>, // !Sync), however, I can't understand what their implications are. Also, what does "!Sync" comment mean?
2. On slide 62: "If the underlying type T is sendable, SpinLock is sharable and sendable". Is this some kind of Rust rule or there is an explanation?
3. 64 why do we need two fences in Peterson's mutex?

Thank you!

I have two questions about casuality test cases.

Problem 3

(Thread1)
r1 = x
r2 = x
if r1 == r2
  y = 1

(Thread3)
x = 2

y=1 can be certified from thread 1. But I confused by thread 3. We can certify the value, even though there is message interleaving from other thread. However, it is possible to y is not assigned to 1 due to thread 3. Doesn't this matter?

Problem 19

This problem is the same as test case 17, except that thread 1 has been split into two threads. I think that join thread plays a similar role as SC fence, but I don't know how it is impossible to recertify. Why is it disallowed by promising semantics?

1. ticketlock이 spinlock과 peterson's mutex의 기능을 합쳐 놓은 느낌인가요?
2. ppt 63page에 "All SC fences are strictly ordered w.r.t the per-thread views"라는 문장의 의미를 자세히 설명해 주세요.
3. ppt 71page에 있는 ticket lock과 MCS parking lock에 대해 다시 한 번 설명해 주실 수 있을까요?
   ---------------------------in english---------------------------------------
4. Does ticketlock feel like a combination of spinlock and peterson's mutex?
5. Please explain in detail the meaning of the sentence "All SC fences are strictly ordered w.r.t the per-thread views" on page 63 of ppt.
6. Could you explain again about the ticket lock and MCS parking lock on page 71 of ppt?

Thankyou :)

I'm wondering how to collect the value out from a nodebox. I'm currently trying by calling '''body.right().unwrap()''' but it says

"cannot move out of a mutable reference

move occurs because value has type V, which does not implement the Copy trait"

How do i get around this ?

I don't really understand the goal of the Cursor function in this case. I understand how the cursor is built but I can't understand what it should do in this case. Is the goal to iterate on the tree here to return the cursor associated with a key ?

This question is about http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html/
By promising semantics, problems in above link is quite easy to solve when behavior is allowed. However, I found that it is quite hard to prove in cases that behavior is disallowed. Do we need to check every ordering of execution in threads to show that the behavior is disallowed? Or is there any better way of showing that behavior is disallowed?

Also, one of term that was mentioned in previous lecture was interleaving semantic. Will it be covered in later lectures? If not, is there some sources to learn about interleaving semantic?

I have a confusion with the meaning of 'mutual exclusion'
In this slide, does it mean same as '&self' that reference to the simultaneous writing of a memory address?

Dear Professor Jeehoon Kang

Could you, please, answer the following questions:

1. On the slide 8, What is SMS? Is it Shared Mutable States?
2. How concurrency is used in parallel computing? In my understanding, parallelism means multiple processes being executed simultaneously, and concurrency, it's when processes are executed in the interleaving fashion, not simultaneously. So, I am confused about how concurrency and parallelism work together on the example of the concurrent queue in Rabbitmq(slide 8), and how concurrency is used in parallel computing?

Thank you!

From the semantics, after executing fence(SC) both the thread view and the global view have to be updated to maximum of them.

Then, I think the SC view in this image also should be updated to X=1, Y=1.

Is it right?

The main content of today's video lecture was mainly IRIS operational semantics which is presented as an alternative to advanced separation logic semantics. The video lecture is in the scope of midterm exam as TA said. So, are we expected to be able to make proofs with various operational semantic variants presented in the lecture?

Thank you!