国产日韩欧美一区二区三区三州_亚洲少妇熟女av_久久久久亚洲av国产精品_波多野结衣网站一区二区_亚洲欧美色片在线91_国产亚洲精品精品国产优播av_日本一区二区三区波多野结衣 _久久国产av不卡

?

使用模型檢測(cè)方法對(duì)Paxos算法進(jìn)行驗(yàn)證與改進(jìn)

2022-05-10 08:45:42何東煉楊晉吉趙淦森管金平
關(guān)鍵詞:檢測(cè)器消息安全性

何東煉,楊晉吉,趙淦森,管金平

(華南師范大學(xué) 計(jì)算機(jī)學(xué)院,廣州 510631)

1 引 言

分布式是實(shí)現(xiàn)橫向拓展,提升系統(tǒng)性能和可靠性的重要技術(shù)理論.現(xiàn)實(shí)實(shí)現(xiàn)中,分布式系統(tǒng)難以在分區(qū)失效、通信故障情況下對(duì)特定的狀態(tài)形成全局共識(shí)和一致性,因此系統(tǒng)需要使用共識(shí)算法[1]來(lái)保證系統(tǒng)內(nèi)的節(jié)點(diǎn)達(dá)成一致的狀態(tài).Paxos算法[2]是Lamport提出的一種共識(shí)算法,主要用于解決基于消息傳遞通信模型的分布式系統(tǒng)如何就某個(gè)值達(dá)成一致的共識(shí),由于其在數(shù)據(jù)一致性方面的優(yōu)秀表現(xiàn),已被應(yīng)用于許多重要的分布式服務(wù)中,并且存在多種變體.

Paxos算法在工業(yè)應(yīng)用中具有明顯優(yōu)勢(shì)并達(dá)到良好的性能和效果,因此對(duì)其進(jìn)行深度的形式化分析和證明[3]工作至關(guān)重要.由于算法問(wèn)題的復(fù)雜性,非形式化的證明往往容易出錯(cuò),而形式化的驗(yàn)證,能夠更好地對(duì)算法的性質(zhì)進(jìn)行分析與研究.模型檢測(cè)[4]是形式化驗(yàn)證的主要方法之一,能夠窮舉目標(biāo)模型的狀態(tài)空間,以確定目標(biāo)是否滿足所需性質(zhì),常用于分布式系統(tǒng)的驗(yàn)證[5].

本文首先對(duì)Paxos算法及其研究進(jìn)展進(jìn)行介紹,然后根據(jù)算法流程對(duì)其進(jìn)行形式化建模,以時(shí)態(tài)邏輯對(duì)算法的安全性、活性和活鎖可能性進(jìn)行描述,將模型與需要驗(yàn)證的性質(zhì)輸入模型檢測(cè)器進(jìn)行驗(yàn)證.驗(yàn)證結(jié)果表明,Paxos算法滿足安全性和活性,但在運(yùn)行過(guò)程中有發(fā)生活鎖的可能,通過(guò)模型檢測(cè)器重現(xiàn)了發(fā)生活鎖時(shí)系統(tǒng)的運(yùn)行軌跡并對(duì)其進(jìn)行分析,最后對(duì)Paxos算法進(jìn)行改進(jìn),解決其活鎖問(wèn)題并重新進(jìn)行驗(yàn)證.

2 Paxos算法及其研究進(jìn)展

隨著分布式系統(tǒng)的迅速發(fā)展和廣泛應(yīng)用,用于分布式系統(tǒng)保持一致性的共識(shí)算法的研究和討論也越來(lái)越多.Paxos算法最初由Lamport提出,之后學(xué)者們便不斷對(duì)該算法進(jìn)行改進(jìn),較為知名的有Multi-Paxos、Fast-Paxos、EPaxos、Raft等[6].Google的spanner[7]使用Multi-Paxos作為分布式共識(shí)保證的基礎(chǔ)組件,PaxosStore[8]是騰訊開發(fā)的、用于支持微信核心業(yè)務(wù)的分布式存儲(chǔ)系統(tǒng).此外,Paxos算法也經(jīng)常應(yīng)用于軟件定義網(wǎng)絡(luò)及區(qū)塊鏈研究[9,10].

目前,已有學(xué)者對(duì)Paxos算法的形式化驗(yàn)證進(jìn)行了一些相關(guān)的工作,近年來(lái)的相關(guān)研究有:文獻(xiàn)[11]使用SPIN對(duì)Paxos進(jìn)行了建模,以斷言的方式驗(yàn)證了算法的安全性.文獻(xiàn)[12]使用TLAPS驗(yàn)證Multi-Paxos 的安全性.文獻(xiàn)[13]使用有色Petri網(wǎng)對(duì)Paxos算法生成自動(dòng)測(cè)試用例.文獻(xiàn)[14]開發(fā)了一種基于有效命題邏輯的演繹驗(yàn)證方法,對(duì)Paxos及其幾種變體的安全性進(jìn)行了驗(yàn)證.文獻(xiàn)[15]構(gòu)建了Paxos的Heard-Of模型,使用PSync語(yǔ)言驗(yàn)證了模型的安全性和活性.文獻(xiàn)[16]使用IronFleet對(duì)以Multi-Paxos為核心的狀態(tài)機(jī)復(fù)制系統(tǒng)進(jìn)行驗(yàn)證,證明了其安全性和活性.文獻(xiàn)[17]使用交互式定理證明系統(tǒng)Coq對(duì)Paxos進(jìn)行了安全性的驗(yàn)證.

而本文的主要工作有:

1)使用SPIN對(duì)Paxos算法進(jìn)行形式化建模,以線性時(shí)序邏輯(Linear-time Temporal Logic,LTL)對(duì)算法的安全性、活性和活鎖的性質(zhì)進(jìn)行描述.

2)對(duì)Paxos算法性質(zhì)進(jìn)行驗(yàn)證分析,還原算法不滿足性質(zhì)時(shí)的運(yùn)行軌跡.

3)對(duì)Paxos算法進(jìn)行改進(jìn),使算法滿足所需的性質(zhì),并重新進(jìn)行驗(yàn)證.

3 對(duì)Paxos算法進(jìn)行模型檢測(cè)

在模型檢測(cè)中,驗(yàn)證目標(biāo)是否滿足某種性質(zhì),通常包含以下3個(gè)步驟:

1)建模.將需要進(jìn)行驗(yàn)證的目標(biāo)轉(zhuǎn)化為能被模型檢測(cè)器接受的模型.如果模型過(guò)于復(fù)雜,會(huì)發(fā)生狀態(tài)空間爆炸問(wèn)題,即系統(tǒng)過(guò)于復(fù)雜導(dǎo)致狀態(tài)過(guò)多使驗(yàn)證失敗,因此需要使用抽象或偏序約簡(jiǎn)等技術(shù)對(duì)模型進(jìn)行化簡(jiǎn).

2)規(guī)約.把目標(biāo)需要驗(yàn)證的性質(zhì)用時(shí)態(tài)邏輯表達(dá)式來(lái)進(jìn)行表述.線性時(shí)序邏輯是常用的時(shí)態(tài)邏輯.

3)驗(yàn)證.將模型和時(shí)態(tài)邏輯表達(dá)式作為模型檢測(cè)器的輸入,運(yùn)行檢測(cè)器并檢驗(yàn)結(jié)果.如果模型不滿足性質(zhì),檢測(cè)器通??梢蕴峁┮粋€(gè)模型不滿足性質(zhì)時(shí)的運(yùn)行軌跡.

3.1 Paxos算法建模

Paxos算法把系統(tǒng)節(jié)點(diǎn)主要分為proposer,acceptor,和learner這3種角色.proposer提出提案,提案包括提案編號(hào)和提議的值.acceptor接收提案,若提案獲得多數(shù)的acceptor接受,則稱該提案被批準(zhǔn).learner學(xué)習(xí)提案,從acceptor學(xué)習(xí)最新被批準(zhǔn)的提案值.傳遞消息的類型包括prepare,promise,propose,accept.在消息傳遞的過(guò)程中,不考慮消息遭到篡改的情況.

由圖1的算法執(zhí)行流程可知,proposer的工作流程如下:

圖1 Paxos算法執(zhí)行一次的流程

1)proposer發(fā)起一個(gè)編號(hào)N的提案,N全局唯一且單調(diào)遞增.然后向多數(shù)派的acceptor發(fā)送包含N的prepare消息,多數(shù)派即超過(guò)acceptor數(shù)量的一半.消息還會(huì)攜帶發(fā)送者的ID以確定消息的來(lái)源,以下不再贅述.

Proposer→Acceptor:prepare(N)

2)proposer發(fā)送prepare消息后等待接收promise消息,用num1記下收到的消息數(shù),記下收到的promise消息中編號(hào)最大的提案為Nmax.如果等待超時(shí),proposer收到的promise消息數(shù)量不滿足多數(shù)派,則提高提案編號(hào)N并重新發(fā)送prepare消息.如果proposer收到多數(shù)派的promise消息,則發(fā)送包含Nmax,V的propose消息給所有回復(fù)promise的acceptor.Nmax,V分別為收到的promise消息中編號(hào)最大提案的編號(hào)及對(duì)應(yīng)的提案值,如果V為null,則由proposer自行設(shè)定(實(shí)驗(yàn)中令V等于proposer自身的ID).

Acceptor→Proposer:propose(Nmax,V)

3)由于Paxos算法中一個(gè)進(jìn)程可以擔(dān)任多種角色,為了減少模型的狀態(tài)空間,實(shí)驗(yàn)中讓proposer同時(shí)擔(dān)任learner.因此,proposer等待接收accept消息,用num2記下收到的消息數(shù).如果等待超時(shí),proposer收到的accept消息數(shù)量不滿足多數(shù)派,則提高提案編號(hào)N并重新發(fā)送prepare消息.如果proposer收到的accept消息滿足多數(shù)派,則令voteEnd等于true,Value等于V,proposer進(jìn)程結(jié)束.

定義proposer的結(jié)構(gòu)體:

typedef ProposerMachine {

int ID,Value;

chan ch=[chanSize]of{mtype,int,int,int};

bool voteEnd=false;

};

其中ID為機(jī)器編號(hào),Value為該機(jī)器的值,ch為消息信道,能夠存儲(chǔ)的消息量為chanSize,mtype為消息類型,voteEnd為結(jié)束標(biāo)記.

算法中的事件則可用有限狀態(tài)機(jī)的輸入來(lái)表示,依據(jù)進(jìn)程與事件之間的關(guān)系,可以得到狀態(tài)和輸入之間的轉(zhuǎn)移關(guān)系.根據(jù)工作流程可得圖2的proposer狀態(tài)轉(zhuǎn)移模型,其中!表示系統(tǒng)發(fā)送消息,而?表示系統(tǒng)接收消息.

圖2 proposer狀態(tài)轉(zhuǎn)移模型

acceptor的工作流程如下:

1)當(dāng)acceptor收到一個(gè)prepare消息后,檢查消息中的N,若N大于ResN(初始為0),則令ResN等于N,發(fā)送promise消息,消息包含AccN(初始為0)和AccV(初始為null).若N不大于ResN,則忽略該消息.

Acceptor→Proposer:promise(AccN,AccV)

2)當(dāng)acceptor收到一個(gè)propose消息后,若消息中攜帶的編號(hào)N大于或等于ResN,則令A(yù)ccN等于N,AccV等于V,并發(fā)送包含AccV的accept消息給propose以及l(fā)earner.若N小于ResN,則忽略該消息.

Acceptor→Proposer,Learner:accept(AccV)

acceptor的結(jié)構(gòu)體如下:

typedef AcceptorMachine {

int ID,ResN,AccN,AccV;

chan ch=[chanSize]of{mtype,int,int,int};

};

其中ID為機(jī)器編號(hào),ResN為該機(jī)器收到的prepare消息的最高提案編號(hào),AccN和AccV為該機(jī)器的收到的propose消息的編號(hào)最大的提案編號(hào)與提案值,ch為消息信道,可以存儲(chǔ)的消息量為chanSize,mtype為消息類型.acceptor狀態(tài)轉(zhuǎn)移結(jié)構(gòu)模型如圖3所示.

圖3 acceptor狀態(tài)轉(zhuǎn)移模型

3.2 驗(yàn)證屬性的描述及其驗(yàn)證結(jié)果

由于需要就某個(gè)值達(dá)成一致的共識(shí),分布式共識(shí)算法一般需要滿足4個(gè)基本性質(zhì):有效性、一致性、完整性、可終止性.這4個(gè)性質(zhì)可以總結(jié)為安全性和活性,安全性即有效性、一致性以及完整性,活性即可終止性.

首先定義全局變量,實(shí)驗(yàn)中proposer的數(shù)量為2,acceptor的數(shù)量為3,則多數(shù)派major的數(shù)量應(yīng)為2,設(shè)置每個(gè)信道能夠存儲(chǔ)的最大消息量為4,初始輪次round為0.

定義實(shí)驗(yàn)狀態(tài)及其含義如表1所示.

表1 實(shí)驗(yàn)狀態(tài)

1)有效性的驗(yàn)證

有效性即進(jìn)程只能選擇已提出的值,其LTL表達(dá)式為:

validity {(true U(End0 && End1))→(true U [](Goal0 && Goal1))}

檢測(cè)結(jié)果如下:

State-vector 596 byte,depth reached 9999,errors:0

2)一致性的驗(yàn)證

一致性即所有進(jìn)程最終選擇的值都相同,其LTL表達(dá)式為:

agreement{(trueU(End0 && End1))→(trueU[]Goal)}

檢測(cè)結(jié)果如下:

State-vector 596 byte,depth reached 9999,errors:0

3)完整性的驗(yàn)證

完整即進(jìn)程一旦選取了某個(gè)值,這個(gè)值就不會(huì)再改變.該性質(zhì)可以轉(zhuǎn)化了選取了某個(gè)值后就不會(huì)再次發(fā)起提案,其LTL表達(dá)式為:

integrity {(End0→[]End0)&&(End1→[]End1)}

檢測(cè)結(jié)果如下:

State-vector 596 byte,depth reached 9999,errors:0

4)可終止性的驗(yàn)證

可終止性即系統(tǒng)中的所有進(jìn)程最終都能夠選擇到某個(gè)值,其LTL表達(dá)式為:

termination{[](trueU(End0&& End1))}

檢測(cè)結(jié)果如下:

State-vector 596 byte,depth reached 9999,errors:0

5)發(fā)生活鎖可能性的驗(yàn)證

檢測(cè)Paxos算法發(fā)生活鎖可能性,即檢測(cè)在有限的次數(shù)內(nèi)Paxos算法是否能得到終止.假設(shè)發(fā)起提案的最大次數(shù)maxRound為50,LTL表達(dá)式為:

livelock{!((!End0&& !End1)Uround>maxRound)}

檢測(cè)結(jié)果如下:

State-vector 596 byte,depth reached 3536,errors:1

檢測(cè)表明算法并不能在限定的最大次數(shù)內(nèi)結(jié)束.圖4為檢測(cè)器還原的算法不滿足驗(yàn)證性質(zhì)時(shí)的運(yùn)行軌跡.

圖4 發(fā)生活鎖時(shí)的運(yùn)行軌跡(部分)

由圖4可知,Paxos算法運(yùn)行過(guò)程中,當(dāng)acceptor對(duì)一個(gè)提案A發(fā)送promise消息后,如果再接到另一個(gè)編號(hào)更高的提案B的prepare請(qǐng)求,將再次進(jìn)行promise,此時(shí),提案A的propose請(qǐng)求將被忽略,然后發(fā)送的提案A的proposer再次提高編號(hào)進(jìn)行prepare請(qǐng)求,這樣兩個(gè)proposer會(huì)交替提高編號(hào)進(jìn)行prepare請(qǐng)求,導(dǎo)致產(chǎn)生活鎖.

4 改進(jìn)Paxos算法以解決活鎖問(wèn)題

分布式系統(tǒng)應(yīng)用一般需要連續(xù)確定多個(gè)值,由于Paxos算法有產(chǎn)生活鎖的可能,直接使用會(huì)造成效率低下,因此在實(shí)際的應(yīng)用中一般采用Multi-Paxos算法.

Multi-Paxos算法即使用一系列的Paxos算法實(shí)例來(lái)確定一系列的值.由于Paxos算法存在活鎖問(wèn)題的主要原因是各個(gè)進(jìn)程可以公平地發(fā)起提案請(qǐng)求,導(dǎo)致各個(gè)進(jìn)程可以交替地提高編號(hào)發(fā)起提案,于是Multi-Paxos算法通過(guò)選舉leader的方式,讓proposer提案請(qǐng)求發(fā)送給leader,然后leader充當(dāng)原來(lái)proposer的職能執(zhí)行Paxos算法.這樣沒(méi)有proposer競(jìng)爭(zhēng)發(fā)起提案,因此可以解決活鎖問(wèn)題.

Multi-Paxos算法并沒(méi)有詳細(xì)說(shuō)明如何進(jìn)行選舉,本文使用一種基于優(yōu)先級(jí)的選舉算法對(duì)Paxos進(jìn)行類Multi-Paxos改進(jìn)并重新進(jìn)行驗(yàn)證.設(shè)置proposer使其擁有各自的優(yōu)先級(jí),在proposer發(fā)起提案請(qǐng)求之前,先向其他所有的proposer發(fā)送hello消息查找自己的leader,其他proposer收到hello消息后,回應(yīng)ack消息,消息包含自己的優(yōu)先級(jí).當(dāng)proposer收到ack消息后將優(yōu)先級(jí)最大的proposer作為自己的leader,然后讓leader代替自己發(fā)起提案.算法改進(jìn)后的流程如圖5所示.

圖5 改進(jìn)Paxos算法執(zhí)行一次的流程(選舉后)

算法改進(jìn)后的proposer的工作流程如下:

1)proposer進(jìn)程運(yùn)行后將啟動(dòng)兩個(gè)線程:listener與leader.

2)proposer準(zhǔn)備發(fā)起請(qǐng)求.若此時(shí)沒(méi)有確定leader,將向其他proposer的listener線程發(fā)送hello消息,收到ack消息后將最高優(yōu)先級(jí)的proposer(可以為自身)作為leader.

Proposer→Listener:hello()

若已確定leader,則向leader發(fā)送request消息.

Proposer→Leader:request()

3)proposer等待接收accept消息,用num2記下收到的消息數(shù).如果等待超時(shí),proposer收到的accept消息數(shù)量不滿足多數(shù)派,則認(rèn)為leader狀態(tài)不佳.重新確定leader后再次發(fā)送request消息.如果proposer收到的accept消息滿足多數(shù)派,則表明提案被選定,令Value等于V,proposer進(jìn)程結(jié)束.

listener的工作流程如下:

listener線程等待接收其他proposer的hello消息,收到消息后會(huì)回復(fù)帶有proposer優(yōu)先級(jí)的ack消息.

Listener→Proposer:ack(priority)

leader的工作流程如下:

1)leader線程等待接收到request消息,收到消息后發(fā)起一個(gè)編號(hào)N的提案,N為全局唯一且單調(diào)遞增.然后向多數(shù)派的acceptor發(fā)送包含N的prepare消息.

Leader→Acceptor:prepare(N)

2)leader等待接收promise消息.收到promise消息后,用num1記下收到的消息數(shù),記下收到的promise消息中編號(hào)最大的提案為Nmax.如果等待超時(shí),leader收到的promise消息數(shù)量不滿足多數(shù)派,則提高提案編號(hào)N并重新發(fā)送prepare消息.如果leader收到多數(shù)派的promise消息,則發(fā)送propose消息給所有回復(fù)promise的acceptor,消息包含Nmax,V及發(fā)起request消息的proposer的ID.Nmax,V分別為收到的promise消息中編號(hào)最大提案的編號(hào)及其對(duì)應(yīng)的提案值,如果V為null,則由leader自行設(shè)定(實(shí)驗(yàn)中令V等于leader自身的ID).

Leader→Acceptor:propose(Nmax,V,IDproposer)

修改proposer的結(jié)構(gòu)體如下:

typedef ProposerMachine {

int ID,Value,priority;

chan ch=[chanSize] of { mtype,int,int,int };

bool voteEnd=false;

};

圖6為子線程listener與leader的狀態(tài)轉(zhuǎn)移模型.

圖6 listener和leader狀態(tài)轉(zhuǎn)移模型

改進(jìn)后proposer的狀態(tài)轉(zhuǎn)移模型如圖7所示.

圖7 改進(jìn)后的proposer狀態(tài)轉(zhuǎn)移模型

acceptor的工作流程如下:

1)當(dāng)acceptor收到一個(gè)prepare消息后,檢查消息中的N,若N大于ResN(初始為0),則令ResN等于N,發(fā)送promise消息,消息包含AccN(初始為0)和AccV(初始為null).若N不大于ResN,則忽略該消息.

Acceptor→Leader:promise(AccN,AccV)

2)當(dāng)acceptor收到一個(gè)propose消息后,若消息中攜帶的編號(hào)N大于或等于ResN,則令A(yù)ccN等于N,AccV等于V,并直接發(fā)送包含AccV的accept消息給發(fā)起request消息的proposer.若N小于ResN,則忽略該消息.

Acceptor→Proposer:accept(AccV)

改進(jìn)后的acceptor狀態(tài)轉(zhuǎn)移模型基本沒(méi)有變化.

設(shè)置proposer的優(yōu)先級(jí)等于其ID值,重新將模型輸入,檢測(cè)Paxos算法發(fā)生活鎖可能性.

檢測(cè)結(jié)果如下:

State-vector 988 byte,depth reached 1049,errors:0

模型檢測(cè)器沒(méi)有發(fā)現(xiàn)錯(cuò)誤,即沒(méi)有發(fā)生活鎖問(wèn)題.

5 結(jié) 語(yǔ)

本文以Paxos算法作為研究對(duì)象,基于模型檢測(cè)工具SPIN,對(duì)算法進(jìn)行了形式化建模,并對(duì)該算法的安全性、活性、發(fā)生活鎖可能性使用LTL語(yǔ)言進(jìn)行了描述,經(jīng)過(guò)分析驗(yàn)證,結(jié)果表明Paxos算法滿足安全性和活性,但存在發(fā)生活鎖的可能,并重現(xiàn)了活鎖發(fā)生時(shí)模型的運(yùn)行軌跡.為了解決Paxos算法發(fā)生的活鎖問(wèn)題,本文使用了一種為proposer添加優(yōu)先級(jí)的類Multi-Paxos改進(jìn)算法,通過(guò)選舉leader的方式,讓leader代替proposer提交提案.該方法優(yōu)點(diǎn)是增加了算法的靈活性,可以指定不同proposer的優(yōu)先級(jí),在實(shí)際應(yīng)用中,優(yōu)先級(jí)可以根據(jù)相應(yīng)的權(quán)重算法進(jìn)行動(dòng)態(tài)調(diào)整,從而實(shí)現(xiàn)proposer的負(fù)載均衡,經(jīng)驗(yàn)證,當(dāng)leader單一存在時(shí),可以解決Paxos算法中發(fā)生的活鎖現(xiàn)象.由于可能存在優(yōu)先級(jí)相同及網(wǎng)絡(luò)不佳等問(wèn)題,可能會(huì)發(fā)生同時(shí)存在多l(xiāng)eader情況,然而即便如此也能大幅降低可能發(fā)生的活鎖現(xiàn)象,當(dāng)所有proposer的優(yōu)先級(jí)一樣時(shí),改進(jìn)后的算法會(huì)退化為普通的paxos算法,即每個(gè)proposer成為自身的leader.

Paxos算法可以應(yīng)用在許多場(chǎng)景中,由于Paxos算法的復(fù)雜性,對(duì)其進(jìn)行形式化建模與驗(yàn)證后,可以使Paxos算法獲得更高的可信度,以及更好地研究該算法在不同場(chǎng)景與范圍中的應(yīng)用情況.同時(shí),Paxos存在很多變種算法,今后的工作可以以本文的Paxos算法模型為基礎(chǔ)或參考,對(duì)Paxos的改進(jìn)算法進(jìn)行驗(yàn)證與分析.

猜你喜歡
檢測(cè)器消息安全性
新染料可提高電動(dòng)汽車安全性
某既有隔震建筑檢測(cè)與安全性鑒定
一張圖看5G消息
車道微波車輛檢測(cè)器的應(yīng)用
ApplePay橫空出世 安全性遭受質(zhì)疑 拿什么保護(hù)你,我的蘋果支付?
一種霧霾檢測(cè)器的研究與設(shè)計(jì)
Imagination發(fā)布可實(shí)現(xiàn)下一代SoC安全性的OmniShield技術(shù)
消息
消息
消息
达日县| 桓台县| 静海县| 隆德县| 独山县| 青铜峡市| 岳普湖县| 黄陵县| 类乌齐县| 承德县| 龙山县| 淮北市| 涪陵区| 武夷山市| 乌拉特中旗| 平山县| 准格尔旗| 始兴县| 曲沃县| 宁远县| 敦煌市| 延安市| 平塘县| 竹山县| 舟曲县| 嘉义县| 和政县| 澄江县| 龙山县| 五寨县| 香格里拉县| 云南省| 西平县| 洮南市| 潮州市| 民和| 汝阳县| 牡丹江市| 康马县| 易门县| 射洪县|