#include <unrelacy.h>
-/**
- Properties to check:
- 1. At any point, only one thread can acquire the mutex; when any thread
- nlock the mutex, he must have it in his hand.
- 2. The sequence of the lock is guaranteed, which means there is a queue for
- all the lock operations.
- ####
- 3. Should establish the happens-before relationship between unlock and lock
-*/
-/**
- @Begin
- @Global_define:
- # The invariant is that the thread that has a guard at the head of the
- # queue should be the one who currently has the lock.
-
- int __lock_acquired = 0;
- queue<guard*> __lock_waiting_queue;
-
- @Happens-before:
- # Without any specifying, this means the beginning of a successful Unlock()
- # happens before the end of the next successful Lock().
- Unlock -> Lock
- @End
-*/
struct mcs_node {
std::atomic<mcs_node *> next;
}
};
+
struct mcs_mutex {
public:
// tail is null when lock is not held
std::atomic<mcs_node *> m_tail;
mcs_mutex() {
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
m_tail.store( NULL );
}
~mcs_mutex() {
~guard() { m_t->unlock(this); }
};
+ /**
+ @Begin
+ @Options:
+ LANG = CPP;
+ CLASS = mcs_mutex;
+ @Global_define:
+ @DeclareVar:
+ bool _lock_acquired;
+ @InitVar:
+ _lock_acquired = false;
+ @Happens_before:
+ Unlock -> Lock
+ @End
+ */
/**
@Begin
- # This function will soon enqueue the current guard to the queue to make
- # sure it will get fair lock successfully.
@Interface: Lock
- @Commit_point_set: Lock_Enqueue_Point
+ @Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
+ @Check:
+ _lock_acquired == false;
@Action:
- @Code:
- __lock_waiting_queue.enqueue(I);
- @Post_action:
- __lock_acquired++;
- @Post_check:
- # Make sure when it successfully locks, the lock is not acquired yet
- # and the locking is in a FIFO order
- __lock_acquired == 1 && I == __lock_waiting_queue.peak()
+ _lock_acquired = true;
@End
*/
void lock(guard * I) {
// publish my node as the new tail :
mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
/**
- # Once the exchange completes, the thread already claimed the next
- # available slot for the lock
@Begin
- @Commit_point_check_define: true
- @Label: Lock_Enqueue_Point
+ @Commit_point_define_check: pred == NULL
+ @Label: Lock_Enqueue_Point1
@End
*/
if ( pred != NULL ) {
// wait on predecessor setting my flag -
rl::linear_backoff bo;
int my_gate = 1;
- while ( (my_gate = me->gate.load(std::mo_acquire)) ) {
+ while (my_gate ) {
+ my_gate = me->gate.load(std::mo_acquire);
+ /**
+ @Begin
+ @Commit_point_define_check: my_gate == 0
+ @Label: Lock_Enqueue_Point2
+ @End
+ */
thrd_yield();
}
}
@Begin
@Interface: Unlock
@Commit_point_set:
- Unlock = Unlock_Point_Success_1 | Unlock_Point_Success_2
+ Unlock_Point_Success_1 | Unlock_Point_Success_2
@Check:
- lock_acquired == 1 && I == lock_waiting_queue.peak()
+ _lock_acquired == true
@Action:
- @Code:
- lock_acquired--;
- lock_waiting_queue.dequeue();
+ _lock_acquired = false;
@End
*/
void unlock(guard * I) {
{
mcs_node * tail_was_me = me;
bool success;
- if ( (success = m_tail.compare_exchange_strong(
- tail_was_me,NULL,std::mo_acq_rel)) ) {
- /**
- @Begin
- @Commit_point_check_define: __ATOMIC_RET__ == true
- @Label: Unlock_Point_Success_1
- @End
- */
+ success = m_tail.compare_exchange_strong(
+ tail_was_me,NULL,std::mo_acq_rel);
+ /**
+ @Begin
+ @Commit_point_define_check: success == true
+ @Label: Unlock_Point_Success_1
+ @End
+ */
+ if (success) {
+
// got null in tail, mutex is unlocked
return;
}
next->gate.store( 0, std::mo_release );
/**
@Begin
- @Commit_point_check_define: true
+ @Commit_point_define_check: true
@Label: Unlock_Point_Success_2
@End
*/
}
};
+/**
+ @Begin
+ @Class_end
+ @End
+*/
new ArrayList<CodeAddition>());
}
codeAdditions.get(defineConstruct.file).add(addition);
- } else { // No declaration needed but should add forward declaration
+ } else { // No declaration needed but should add forward declaration in
+ // Class
// Last generate the definition
newCode = new ArrayList<String>();
- newCode.addAll(CodeVariables.generateInterfaceWrapperDeclaration(_semantics, construct));
+ if (_semantics.getOption("CLASS") == null) {
+ newCode.addAll(CodeVariables
+ .generateInterfaceWrapperDeclaration(_semantics,
+ construct));
+ }
newCode.addAll(CodeVariables.generateInterfaceWrapperDefinition(
_semantics, construct));
lineNum = construct.beginLineNum;
codeAdditions.get(construct.file).add(addition);
}
+ /**
+ private void ClassEnd2Code(ClassEndConstruct construct) {
+ int lineNum = construct.beginLineNum;
+ ArrayList<String> newCode = CodeVariables.generateStaticVarDefine(_semantics,
+ _semantics.getGlobalConstruct());
+
+ CodeAddition addition = new CodeAddition(lineNum, newCode);
+ if (!codeAdditions.containsKey(construct.file)) {
+ codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
+ }
+ codeAdditions.get(construct.file).add(addition);
+ }
+ */
+
private void EntryPoint2Code(EntryPointConstruct construct) {
int lineNum = construct.beginLineNum;
ArrayList<String> newCode = new ArrayList<String>();
EntryPoint2Code((EntryPointConstruct) construct);
}
}
+
+// ClassEndConstruct endConstruct = _semantics.getClassEndConstruct();
+// if (endConstruct != null) {
+// ClassEnd2Code(endConstruct);
+// }
+
// Sort code additions
HashSet<String> headers = CodeVariables.getAllHeaders(_semantics);
ArrayList<String> headerCode = new ArrayList<String>(headers.size());
public static void main(String[] argvs) {
String homeDir = Environment.HOME_DIRECTORY;
File[] srcFiles = {
-// new File(homeDir
-// + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
- // new File(homeDir
- // +
- // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
- // };
- new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
- new File(homeDir + "/benchmark/ms-queue/main.c"),
- new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
-
-// new File(homeDir + "/benchmark/read-copy-update/rcu.cc") };
-
-// new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.c"),
-// new File(homeDir + "/benchmark/chase-lev-deque-bugfix/main.c"),
-// new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.h") };
-
+ // new File(homeDir
+ // + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+ // new File(homeDir
+ // +
+ // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
+ // };
+ // new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+ // new File(homeDir + "/benchmark/ms-queue/main.c"),
+ // new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+
+ // new File(homeDir + "/benchmark/read-copy-update/rcu.cc") };
+
+ // new File(homeDir +
+ // "/benchmark/chase-lev-deque-bugfix/deque.c"),
+ // new File(homeDir +
+ // "/benchmark/chase-lev-deque-bugfix/main.c"),
+ // new File(homeDir +
+ // "/benchmark/chase-lev-deque-bugfix/deque.h") };
+
+ new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"),
+ new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") };
+
CodeGenerator gen = new CodeGenerator(srcFiles);
gen.generateCode();
}
String interfaceSize = Integer
.toString(semantics.interfaceName2Construct.size());
newCode.add(DEFINE("INTERFACE_SIZE", interfaceSize));
- newCode.add(DECLARE("void**", "func_ptr_table"));
+ // Make it static
+ newCode.add("static " + DECLARE("void**", "func_ptr_table"));
// Happens-before initialization rules
- newCode.add(DECLARE(ANNO_HB_INIT + "**", "hb_init_table"));
+ // Should make it static
+ newCode.add("static " + DECLARE(ANNO_HB_INIT + "**", "hb_init_table"));
newCode.add("");
newCode.add(COMMENT("Define function for sequential code initialization"));
String templateDecl = semantics.getTemplateFullStr();
if (templateList == null) {
newCode.add(DECLARE("void**", varPrefix + "func_ptr_table"));
- newCode.add(DECLARE("void**", varPrefix + "hb_init_table"));
+ newCode.add(DECLARE("anno_hb_init**", varPrefix + "hb_init_table"));
for (int i = 0; i < construct.code.declareVar.size(); i++) {
VariableDeclaration varDecl = construct.code.declareVar.get(i);
newCode.add(DECLARE(varDecl.type, varPrefix + varDecl.name));
private ArrayList<EntryPointConstruct> entryPointConstructs;
private ClassBeginConstruct classBeginConstruct;
private ClassEndConstruct classEndConstruct;
+ private GlobalConstruct globalConstruct;
private String templateStr;
private String templateFullStr;
public String getClassName() {
return this.className;
}
+
+ public GlobalConstruct getGlobalConstruct() {
+ return this.globalConstruct;
+ }
public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
return this.hbConditions;
Construct construct = constructs.get(i);
if (construct instanceof GlobalConstruct) {
GlobalConstruct theConstruct = (GlobalConstruct) construct;
+ globalConstruct = theConstruct;
if (!hasGlobalConstruct)
hasGlobalConstruct = true;
else {
} else if (construct instanceof ClassEndConstruct) {
classEndConstruct = (ClassEndConstruct) construct;
+ className = getOption("CLASS");
}
}
}
projects / cdsspec-compiler.git / commitdiff